Theorem 2an 72

Description: Conjoin both sides of hypotheses.

Hypotheses

Ref	Expression
2an.1	a = b
2an.2	c = d

Assertion

Ref	Expression
2an	(a ^ c) = (b ^ d)

Proof of Theorem 2an

Step	Hyp	Ref	Expression
1		2an.2	. . 3 c = d
2	1	lan 70	. 2 (a ^ c) = (a ^ d)
3		2an.1	. . 3 a = b
4	3	ran 71	. 2 (a ^ d) = (b ^ d)
5	2, 4	ax-r2 35	1 (a ^ c) = (b ^ d)

Syntax hints:   = wb 1   ^ wa 7

This theorem is referenced by:  dfnb 87  conb 114  di 118  ledior 169  wwcomd 206  wwcom3ii 207  wwfh1 208  ka4lemo 220  wlem1 235  i3n1 241  ni31 242  ri3 245  ud4lem0a 254  i1i2 258  i3i4 262  i5con 264  ud4lem0c 272  ud5lem0c 273  nomb41 291  nomb32 292  nomcon0 293  nomcon1 294  nomcon2 295  nom21 306  nom22 307  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  2vwomr2 344  2vwomlem 347  wr5-2v 348  wdf-c2 366  woml7 419  comd 438  com3ii 439  comcom5 440  fh1 451  fh3 453  fh4 454  fh3r 457  fh4r 458  gsth 471  i3bi 478  dfi4b 482  i3n2 483  ni32 484  oi3ai3 485  i3th1 525  i3con 533  i3orlem5 538  ud1lem1 542  ud2lem1 545  ud2lem3 547  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem1 571  ud5lem3c 575  ud5lem3 576  u4lemona 610  u3lemob 614  u4lemob 615  u3lemonb 619  u2lemc4 684  u4lemc4 686  u5lemc4 687  u1lembi 702  u2lembi 703  u5lembi 707  u1lem3var1 713  oi3oa3 715  u4lem1 719  u4lem1n 724  u2lem3 732  u1lem4 739  u4lem5 746  u4lem6 750  u1lem8 758  u1lem11 762  u2lem8 764  u3lem10 767  u3lem13a 771  u3lem13b 772  bi1o1a 780  i2i1i1 782  i1abs 783  test 784  test2 785  3vth5 790  3vth7 792  3vth9 794  1oa 802  1oai1 803  2oai1u 804  2oalem1 807  2oath1i1 809  1oath1i1u 810  mlalem 814  mlaoml 815  bi3 821  bi4 822  orbi 824  mlaconj4 826  mlaconj 827  negant5 845  neg3antlem2 847  comanblem1 852  comanblem2 853  comanbn 855  mhlemlem2 857  mhlem 858  mhlem2 860  mh 861  mlaconjolem 867  distid 869  mhcor1 870  oago3.29 871  gomaex4 880  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem6 899  gomaex3lem7 900  oau 909  oa6v4v 913  oa4v3v 914  oa23 916  distoa 924  oa3to4lem5 929  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa6fromdualn 934  oa6to4 938  oa4to6 945  oa8todual 951  oa8to5 952  oa4to4u 953  oa4uto4g 955  oa4gto4u 956  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-4lem 963  oa3-u1lem 965  oa3-u2lem 966  oa3-2to2s 970  oal2 979  oal1 980  mloa 998  3oa2 1004  4oath1 1020

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