Theorem lan 77

Description: Introduce conjunct on left. (Contributed by NM, 10-Aug-1997.)

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⊥ ∪ a⊥ ) = (c⊥ ∪ b⊥ )
4	3	ax-r4 37	. 2 (c⊥ ∪ a⊥ )⊥ = (c⊥ ∪ b⊥ )⊥
5		df-a 40	. 2 (c ∩ a) = (c⊥ ∪ a⊥ )⊥
6		df-a 40	. 2 (c ∩ b) = (c⊥ ∪ b⊥ )⊥
7	4, 5, 6	3tr1 63	1 (c ∩ a) = (c ∩ b)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

This theorem is referenced by:  ran  78  2an  79  an32  83  an4  86  lbi  97  anandir  115  1b  117  anabs  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  oa3moa3  1029  4oa  1039  4oath1  1041  4oagen1b  1043  4oadist  1044  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i0e1  1057  lem3.3.7i1e2  1061  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.4.3  1076  lem4.6.2e1  1082  lem4.6.6i2j4  1097  wdcom  1105  mldual  1124  ml2i  1125  mldual2i  1127  vneulem1  1131  vneulem12  1142  vneulem13  1143  vneulemexp  1148  modexp  1152  dp15lema  1154  dp15lemc  1156  dp15leme  1158  dp53lema  1163  dp53lemb  1164  dp53lemc  1165  dp53leme  1167  dp53lemf  1168  dp35lemc  1175  dp35lemb  1176  dp41lemc0  1184  dp41lemd  1186  dp41leme  1187  dp41lemg  1189  dp41lemj  1191  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod  1213  testmod1  1214  testmod2  1215  testmod2expanded  1216  testmod3  1217