Theorem ran 71

Description: Introduce conjunct on right.

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 70	. 2 (c ∩ a) = (c ∩ b)
3		ancom 68	. 2 (a ∩ c) = (c ∩ a)
4		ancom 68	. 2 (b ∩ c) = (c ∩ b)
5	2, 3, 4	3tr1 60	1 (a ∩ c) = (b ∩ c)

Syntax hints:   = wb 1   ∩ wa 7

This theorem is referenced by:  2an 72  an12 74  anandi 106  mi 117  lel 143  leran 145  bctr 173  wwfh2 209  ska8 228  i3n1 241  ri3 245  ud1lem0b 248  ud2lem0b 251  ud4lem0b 255  ud5lem0b 257  i3i4 262  i5con 264  wql2lem3 282  wql2lem5 284  nom11 300  nom14 303  nom15 304  nom21 306  nom24 309  nom25 310  2vwomlem 347  ska2 414  ska4 415  woml6 418  omln 428  oml5a 432  comcom 435  com3i 449  fh2 452  fh1rc 461  fh2rc 462  oml4 469  gsth 471  gsth2 472  i3bi 478  dfi3b 481  dfi4b 482  i3n2 483  i3lem1 486  i3le 497  i3abs3 506  ud1lem3 544  ud2lem1 545  ud2lem2 546  ud2lem3 547  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem2 553  ud3lem3b 555  ud4lem1a 559  ud4lem1b 560  ud4lem2 564  ud4lem3a 565  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u1lemana 587  u2lemana 588  u3lemana 589  u4lemana 590  u5lemana 591  u1lemab 592  u2lemab 593  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u4lemoa 605  u4lemnob 655  u1lemle2 697  u4lemle2 700  u5lemle2 701  u21lembi 709  u2lem1 717  u4lem1 719  u4lem1n 724  u1lem2 726  u2lem2 727  u1lem4 739  u4lem6 750  u24lem 752  u1lem7 754  u2lem7 755  u3lem7 756  u1lem11 762  u3lem10 767  u3lem11 768  u3lem15 777  test 784  3vth1 786  3vth4 789  3vth5 790  3vded21 799  1oa 802  1oaiii 805  2oath1 808  oale 811  3vroa 813  mlaoml 815  salem1 819  bi3 821  bi4 822  mlaconj4 826  mlaconj 827  negantlem5 835  negantlem6 836  negant2 840  negantlem10 843  neg3antlem1 846  neg3antlem2 847  comanblem1 852  comanblem2 853  mhlem1 859  mh 861  marsdenlem3 864  mlaconjolem 867  mhcor1 870  cancellem 873  govar 876  gomaex4 880  go2n6 881  gomaex3lem8 901  gomaex3 904  oaidlem2 911  oaidlem2g 912  oa6v4v 913  distoah4 923  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4to4u 953  oa3-1lem 962  oa3-u1lem 965  oa3-1to5 973  oaliii 981  oalem1 985  oacom3 993  oagen1b 995  oadist 999  oadistb 1000  oadistc0 1001  4oagen1b 1022

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