Theorem 2an 79

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 77	. 2 (a ^ c) = (a ^ d)
3		2an.1	. . 3 a = b
4	3	ran 78	. 2 (a ^ d) = (b ^ d)
5	2, 4	ax-r2 36	1 (a ^ c) = (b ^ d)

Syntax hints:   = wb 1   ^ wa 7

This theorem is referenced by:  dfnb 95  conb 122  di 126  ledior 177  wwcomd 214  wwcom3ii 215  wwfh1 216  ka4lemo 228  wlem1 243  i3n1 249  ni31 250  ri3 253  ud4lem0a 262  i1i2 266  i3i4 270  i5con 272  ud4lem0c 280  ud5lem0c 281  nomb41 299  nomb32 300  nomcon0 301  nomcon1 302  nomcon2 303  nom21 314  nom22 315  nom50 331  nom51 332  nom52 333  nom53 334  nom54 335  k1-6 353  k1-7 354  k1-5 360  2vwomr2 362  2vwomlem 365  wr5-2v 366  wdf-c2 384  woml7 437  comd 456  com3ii 457  comcom5 458  fh1 469  fh3 471  fh4 472  fh3r 475  fh4r 476  gsth 489  i3bi 496  dfi4b 500  i3n2 501  ni32 502  oi3ai3 503  i3th1 543  i3con 551  i3orlem5 556  ud1lem1 560  ud2lem1 563  ud2lem3 565  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1d 569  ud3lem1 570  ud3lem2 571  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud4lem2 582  ud4lem3b 584  ud4lem3 585  ud5lem1a 586  ud5lem1b 587  ud5lem1c 588  ud5lem1 589  ud5lem3c 593  ud5lem3 594  u4lemona 628  u3lemob 632  u4lemob 633  u3lemonb 637  u2lemc4 702  u4lemc4 704  u5lemc4 705  u1lembi 720  u2lembi 721  u5lembi 725  u1lem3var1 731  oi3oa3 733  u4lem1 737  u4lem1n 742  u2lem3 750  u1lem4 757  u4lem5 764  u4lem6 768  u1lem8 776  u1lem11 780  u2lem8 782  u3lem10 785  u3lem13a 789  u3lem13b 790  bi1o1a 798  i2i1i1 800  i1abs 801  test 802  test2 803  3vth5 808  3vth7 810  3vth9 812  1oa 820  1oai1 821  2oai1u 822  2oalem1 825  2oath1i1 827  1oath1i1u 828  mlalem 832  mlaoml 833  bi3 839  bi4 840  orbi 842  mlaconj4 844  mlaconj 845  negant5 863  neg3antlem2 865  comanblem1 870  comanblem2 871  comanbn 873  mhlemlem2 875  mhlem 876  mhlem2 878  mh 879  mlaconjolem 885  distid 887  mhcor1 888  oago3.29 889  e2ast2 894  e2astlem1 895  gomaex4 900  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  gomaex3lem6 919  gomaex3lem7 920  oau 929  oa6v4v 933  oa4v3v 934  oa23 936  distoa 944  oa3to4lem5 949  oa3to4lem6 950  oa6todual 952  oa6fromdual 953  oa6fromdualn 954  oa6to4 958  oa4to6 965  oa8todual 971  oa8to5 972  oa4to4u 973  oa4uto4g 975  oa4gto4u 976  oa3-2lema 978  oa3-2lemb 979  oa3-6lem 980  oa3-3lem 981  oa3-4lem 983  oa3-u1lem 985  oa3-u2lem 986  oa3-2to2s 990  oal2 999  oal1 1000  mloa 1018  3oa2 1024  4oath1 1040  lem3.3.4 1052  lem3.3.6 1055  lem4.6.2e1 1079  lem4.6.7 1100

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