Theorem ran 78

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

Hypothesis

Ref	Expression
ran.1	a = b

Assertion

Ref	Expression
ran	(a ∩ c) = (b ∩ c)

Proof of Theorem ran

Step	Hyp	Ref	Expression
1		ran.1	. . 3 a = b
2	1	lan 77	. 2 (c ∩ a) = (c ∩ b)
3		ancom 74	. 2 (a ∩ c) = (c ∩ a)
4		ancom 74	. 2 (b ∩ c) = (c ∩ b)
5	2, 3, 4	3tr1 63	1 (a ∩ c) = (b ∩ c)

Syntax hints:   = wb 1   ∩ 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:  2an  79  an12  81  anandi  114  mi  125  lel  151  leran  153  bctr  181  wwfh2  217  ska8  236  i3n1  249  ri3  253  ud1lem0b  256  ud2lem0b  259  ud4lem0b  263  ud5lem0b  265  i3i4  270  i5con  272  wql2lem3  290  wql2lem5  292  nom11  308  nom14  311  nom15  312  nom21  314  nom24  317  nom25  318  k1-6  353  k1-7  354  k1-8a  355  k1-8b  356  k1-2  357  k1-3  358  k1-5  360  2vwomlem  365  ska2  432  ska4  433  woml6  436  omln  446  oml5a  450  comcom  453  com3i  467  fh2  470  fh1rc  479  fh2rc  480  oml4  487  gsth  489  gsth2  490  i3bi  496  dfi3b  499  dfi4b  500  i3n2  501  i3lem1  504  i3le  515  i3abs3  524  ud1lem3  562  ud2lem1  563  ud2lem2  564  ud2lem3  565  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem2  571  ud3lem3b  573  ud4lem1a  577  ud4lem1b  578  ud4lem2  582  ud4lem3a  583  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1c  588  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  ud5lem3c  593  u1lemaa  600  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u1lemana  605  u2lemana  606  u3lemana  607  u4lemana  608  u5lemana  609  u1lemab  610  u2lemab  611  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u4lemoa  623  u4lemnob  673  u1lemle2  715  u4lemle2  718  u5lemle2  719  u21lembi  727  u2lem1  735  u4lem1  737  u4lem1n  742  u1lem2  744  u2lem2  745  u1lem4  757  u4lem6  768  u24lem  770  u1lem7  772  u2lem7  773  u3lem7  774  u1lem11  780  u3lem10  785  u3lem11  786  u3lem15  795  test  802  3vth1  804  3vth4  807  3vth5  808  3vded21  817  1oa  820  1oaiii  823  2oath1  826  oale  829  3vroa  831  mlaoml  833  salem1  837  bi3  839  bi4  840  mlaconj4  844  mlaconj  845  negantlem5  853  negantlem6  854  negant2  858  negantlem10  861  neg3antlem1  864  neg3antlem2  865  comanblem1  870  comanblem2  871  mhlem1  877  mh  879  marsdenlem3  882  mlaconjolem  885  mhcor1  888  cancellem  891  govar  896  gomaex4  900  go2n6  901  gomaex3lem8  921  gomaex3  924  oaidlem2  931  oaidlem2g  932  oa6v4v  933  distoah4  943  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to4u  973  oa3-1lem  982  oa3-u1lem  985  oa3-1to5  993  oaliii  1001  oalem1  1005  oacom3  1013  oagen1b  1015  oadist  1019  oadistb  1020  oadistc0  1021  4oagen1b  1043  lem3.3.4  1053  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e2  1070  lem3.4.3  1076  thm3.8i1lem  1080  lem4.6.2e1  1082  lem4.6.6i1j3  1094  mli  1126  mlduali  1128  vneulem2  1132  vneulem3  1133  vneulem6  1136  vneulemexp  1148  modexp  1152  dp15lema  1154  dp15lemc  1156  dp15lemd  1157  dp53lemb  1164  dp35lemb  1176  dp41leme  1187  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod  1213  testmod2  1215  testmod2expanded  1216