Theorem ran 78

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 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 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 1042  lem3.3.4 1052  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e2 1069  lem3.4.3 1075  lem4.6.2e1 1079  lem4.6.6i1j3 1091

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