QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  2an Unicode version
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
StepHypRef Expression
1 2an.2 . . 3 c = d
21lan 77 . 2 (a ^ c) = (a ^ d)
3 2an.1 . . 3 a = b
43ran 78 . 2 (a ^ d) = (b ^ d)
52, 4ax-r2 36 1 (a ^ c) = (b ^ d)
Colors of variables: term
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:  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  oa3moa3  1029  4oath1  1041  lem3.3.4  1053  lem3.3.6  1056  lem4.6.2e1  1080  lem4.6.7  1101  mldual  1122  vneulem6  1134  vneulem10  1138  vneulem11  1139  vneulem15  1143  vneulem16  1144  vneulemexp  1146  l42modlem1  1147  dp15lemc  1154  dp32  1194  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod  1211  testmod2  1213  testmod2expanded  1214
  Copyright terms: Public domain W3C validator