Theorem lan 70

Description: Introduce conjunct on left.

Hypothesis

Ref	Expression
lan.1	a = b

Assertion

Ref	Expression
lan	(c ^ a) = (c ^ b)

Proof of Theorem lan

Step	Hyp	Ref	Expression
1		lan.1	. . . . 5 a = b
2	1	ax-r4 36	. . . 4 a_|_ = b_|_
3	2	lor 66	. . 3 (c_|_ v a_|_) = (c_|_ v b_|_)
4	3	ax-r4 36	. 2 (c_|_ v a_|_)_|_ = (c_|_ v b_|_)_|_
5		df-a 39	. 2 (c ^ a) = (c_|_ v a_|_)_|_
6		df-a 39	. 2 (c ^ b) = (c_|_ v b_|_)_|_
7	4, 5, 6	3tr1 60	1 (c ^ a) = (c ^ b)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  ran 71  2an 72  an32 76  an4 78  lbi 89  anandir 107  1b 109  a5c 113  leoa 115  mi 117  letr 129  lbtr 131  comm0 170  cbtr 174  comcom2 175  wwoml2 204  wwcom3ii 207  wwfh1 208  wwfh2 209  wwfh3 210  wwfh4 211  lei3 238  i3n1 241  i3id 243  li3 244  ud1lem0a 247  ud2lem0a 250  ud4lem0a 254  ud5lem0a 256  ud2lem0c 270  nom15 304  nom22 307  nom23 308  nom25 310  nom51 324  nom52 325  nom53 326  nom54 327  go1 335  2vwomlem 347  wr5-2v 348  wdf-c1 365  wdf-c2 366  omlan 430  oml5 431  oml5a 432  oml2 433  comcom 435  com3ii 439  fh1 451  fh2 452  fh2c 459  oml4 469  oml6 470  gsth 471  i3bi 478  df2i3 480  dfi3b 481  ni32 484  oi3ai3 485  i3lem1 486  i3lem3 488  lem4 493  i3abs3 506  i3orlem3 536  i3orlem7 540  i3orlem8 541  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem1 545  ud3lem1a 548  ud3lem1b 549  ud3lem1d 551  ud3lem2 553  ud3lem3b 555  ud3lem3d 557  ud4lem1a 559  ud4lem1b 560  ud4lem2 564  ud4lem3a 565  ud5lem1a 568  ud5lem1b 569  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u1lemab 592  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u5lemnaa 626  u3lemnona 649  u1lemc4 683  u3lemc4 685  u4lemc4 686  u5lemc4 687  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u5lembi 707  u12lembi 708  u21lembi 709  oi3oa3lem1 714  oi3oa3 715  u2lem1 717  u4lem1 719  u3lem3 733  u1lem4 739  u4lem4 741  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u24lem 752  u1lem11 762  u2lem8 764  u3lem10 767  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14a 773  u3lem15 777  3vth1 786  3vth2 787  3vth7 792  3vth9 794  3vded12 797  3vded13 798  3vded21 799  3vded3 801  1oa 802  1oaiii 805  1oaii 806  2oalem1 807  2oath1 808  oale 811  mlalem 814  sa5 818  bi3 821  bi4 822  imp3 823  orbi 824  mlaconj4 826  mlaconj 827  negantlem2 831  neg3antlem2 847  elimcons2 851  comanblem1 852  comanblem2 853  mhlemlem1 856  mhlem 858  mhlem1 859  mhlem2 860  mh 861  marsdenlem3 864  marsdenlem4 865  mlaconjo 868  mhcor1 870  cancellem 873  govar 876  go2n4 879  gomaex4 880  go2n6 881  gomaex3lem7 900  gomaex3lem8 901  gomaex3lem9 902  gomaex3 904  oa6v4v 913  oa4v3v 914  oa23 916  distoa 924  oa3to4lem5 929  oa3to4lem6 930  oa6to4 938  oa4dcom 950  oa8to5 952  oa4to4u 953  oa4uto4g 955  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-2to2s 970  d3oa 975  d4oa 976  oaliii 981  oalii 982  oaliv 983  oath1 984  oalem2 986  oadist2a 987  oacom 991  oagen1b 995  oadistb 1000  oadistd 1003  3oa3 1005  4oa 1018  4oath1 1020  4oagen1b 1022  4oadist 1023

This theorem was proved from axioms:  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39

metamath.org