Theorem lan 77

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 37	. . . 4 a' = b'
3	2	lor 70	. . 3 (c' v a') = (c' v b')
4	3	ax-r4 37	. 2 (c' v a')' = (c' v b')'
5		df-a 40	. 2 (c ^ a) = (c' v a')'
6		df-a 40	. 2 (c ^ b) = (c' v b')'
7	4, 5, 6	3tr1 63	1 (c ^ a) = (c ^ b)

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  ran 78  2an 79  an32 83  an4 86  lbi 97  anandir 115  1b 117  a5c 121  leoa 123  mi 125  letr 137  lbtr 139  comm0 178  cbtr 182  comcom2 183  wwoml2 212  wwcom3ii 215  wwfh1 216  wwfh2 217  wwfh3 218  wwfh4 219  anorabs 225  lei3 246  i3n1 249  i3id 251  li3 252  ud1lem0a 255  ud2lem0a 258  ud4lem0a 262  ud5lem0a 264  ud2lem0c 278  nom15 312  nom22 315  nom23 316  nom25 318  nom51 332  nom52 333  nom53 334  nom54 335  go1 343  k1-6 353  k1-7 354  k1-8b 356  k1-4 359  k1-5 360  2vwomlem 365  wr5-2v 366  wdf-c1 383  wdf-c2 384  omlan 448  oml5 449  oml5a 450  oml2 451  comcom 453  com3ii 457  fh1 469  fh2 470  fh2c 477  oml4 487  oml6 488  gsth 489  i3bi 496  df2i3 498  dfi3b 499  ni32 502  oi3ai3 503  i3lem1 504  i3lem3 506  lem4 511  i3abs3 524  i3orlem3 554  i3orlem7 558  i3orlem8 559  ud1lem1 560  ud1lem2 561  ud1lem3 562  ud2lem1 563  ud3lem1a 566  ud3lem1b 567  ud3lem1d 569  ud3lem2 571  ud3lem3b 573  ud3lem3d 575  ud4lem1a 577  ud4lem1b 578  ud4lem2 582  ud4lem3a 583  ud5lem1a 586  ud5lem1b 587  ud5lem2 590  ud5lem3a 591  ud5lem3b 592  ud5lem3c 593  u2lemaa 601  u3lemaa 602  u4lemaa 603  u5lemaa 604  u3lemana 607  u4lemana 608  u5lemana 609  u1lemab 610  u3lemab 612  u4lemab 613  u5lemab 614  u1lemanb 615  u2lemanb 616  u3lemanb 617  u4lemanb 618  u5lemanb 619  u5lemnaa 644  u3lemnona 667  u1lemc4 701  u3lemc4 703  u4lemc4 704  u5lemc4 705  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  u5lembi 725  u12lembi 726  u21lembi 727  oi3oa3lem1 732  oi3oa3 733  u2lem1 735  u4lem1 737  u3lem3 751  u1lem4 757  u4lem4 759  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u24lem 770  u1lem11 780  u2lem8 782  u3lem10 785  u3lem11 786  u3lem13a 789  u3lem13b 790  u3lem14a 791  u3lem15 795  3vth1 804  3vth2 805  3vth7 810  3vth9 812  3vded12 815  3vded13 816  3vded21 817  3vded3 819  1oa 820  1oaiii 823  1oaii 824  2oalem1 825  2oath1 826  oale 829  mlalem 832  sa5 836  bi3 839  bi4 840  imp3 841  orbi 842  mlaconj4 844  mlaconj 845  negantlem2 849  neg3antlem2 865  elimcons2 869  comanblem1 870  comanblem2 871  mhlemlem1 874  mhlem 876  mhlem1 877  mhlem2 878  mh 879  marsdenlem3 882  marsdenlem4 883  mlaconjo 886  mhcor1 888  cancellem 891  e2ast2 894  e2astlem1 895  govar 896  go2n4 899  gomaex4 900  go2n6 901  gomaex3lem7 920  gomaex3lem8 921  gomaex3lem9 922  gomaex3 924  oa6v4v 933  oa4v3v 934  oa23 936  distoa 944  oa3to4lem5 949  oa3to4lem6 950  oa6to4 958  oa4dcom 970  oa8to5 972  oa4to4u 973  oa4uto4g 975  oa3-2lema 978  oa3-2lemb 979  oa3-6lem 980  oa3-3lem 981  oa3-1lem 982  oa3-4lem 983  oa3-5lem 984  oa3-u1lem 985  oa3-u2lem 986  oa3-2to2s 990  d3oa 995  d4oa 996  oaliii 1001  oalii 1002  oaliv 1003  oath1 1004  oalem2 1006  oadist2a 1007  oacom 1011  oagen1b 1015  oadistb 1020  oadistd 1023  3oa3 1025  4oa 1038  4oath1 1040  4oagen1b 1042  4oadist 1043  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i0e1 1056  lem3.3.7i1e2 1060  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.4.3 1075  lem4.6.2e1 1079  lem4.6.6i2j4 1094  wdcom 1102

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

This theorem depends on definitions:  df-a 40

Copyright terms: Public domain