MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2ant2r Structured version   Unicode version

Theorem ad2ant2r 746
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2r  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 716 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 714 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  foco  5795  fvreseq0  5972  fliftfun  6195  omordi  7217  f1imaen2g  7578  isinf  7735  frfi  7767  acndom2  8438  infxp  8598  cff1  8641  isf32lem7  8742  fpwwe2lem12  9022  inawinalem  9070  inar1  9156  grur1  9201  genpnnp  9386  ltexprlem7  9423  prlem936  9428  reclem3pr  9430  1re  9598  addsub4  9867  muladd  9996  lt2add  10044  mullt0  10079  mulnzcnopr  10202  divmuldiv  10251  divmul24  10255  divmuleq  10256  recdiv  10257  divadddiv  10266  conjmul  10268  prodgt0  10394  ltmul12a  10405  lemul12b  10406  lediv12a  10445  lediv2a  10446  qmulcl  11210  irrmul  11217  xrrege0  11385  xmulge0  11486  ge0addcl  11642  ge0mulcl  11643  ge0xaddcl  11644  ge0xmulcl  11645  fzass4  11731  fzrev  11752  fzm1  11768  fzocatel  11861  serge0  12142  expclzlem  12171  expge0  12183  expge1  12184  lt2sq  12222  le2sq  12223  bernneq  12273  wrdeqswrdlsw  12655  cshwleneq  12766  s2eq2seq  12863  sqrmo  13066  limsupval2  13284  o1lo12  13342  climrlim2  13351  2clim  13376  climsup  13473  tanaddlem  13882  divalglem8  14039  opeo  14318  omeo  14319  pcpremul  14348  pcmul  14356  setscom  14643  fpwipodrs  15772  grplactcnv  16116  resgrpisgrp  16200  ghmpreima  16266  ghmeql  16267  conjghm  16275  pgpfi  16603  lmodprop2d  17550  lidlmcl  17843  xrs1mnd  18434  absabv  18453  frlmipval  18787  lmimco  18856  mavmulass  19028  mdetdiaglem  19077  cramerimplem2  19163  opnneissb  19592  cncnpi  19756  pnrmopn  19821  cmpsub  19877  connsub  19899  t1conperf  19914  neitx  20085  txcnmpt  20102  txrest  20109  txdis1cn  20113  tx1stc  20128  qtopcn  20192  trfg  20369  rnelfmlem  20430  flffbas  20473  nmo0  21219  nmoid  21226  cfilfcls  21690  iscmet3lem2  21708  caubl  21723  relcmpcmet  21732  ovolun  21887  ovolicc2lem3  21907  volsup  21943  ioombl1lem4  21948  ismbf3d  22038  mbfimaopnlem  22039  i1faddlem  22077  itgle  22193  ellimc2  22258  ftc1a  22415  dgrmul  22643  itgulm  22779  abelthlem8  22810  ptolemy  22865  logdivlt  22982  cxplt3  23057  cxple3  23058  o1cxp  23280  basellem4  23333  sqf11  23389  lgslem3  23549  lgsdir2  23579  lgsne0  23584  lgsquad3  23612  chpo1ubb  23642  vmadivsumb  23644  rpvmasumlem  23648  dchrisum0re  23674  dchrisum0  23681  selberg2b  23713  selberg3lem2  23719  pntrsumbnd  23727  pntrlog2bnd  23745  axcontlem2  24244  usgra2adedgspth  24589  2wlkeq  24683  wwlkext2clwwlk  24779  grporcan  25199  isgrp2d  25213  ablomul  25333  blocni  25696  ubthlem3  25764  htthlem  25810  hvsub4  25930  shscli  26211  elspansn4  26467  5oalem2  26549  hosub4  26708  hmops  26915  hmopco  26918  adjadd  26988  hstpyth  27124  hstles  27126  mdsl0  27205  mdslmd1lem2  27221  chirredlem1  27285  chirredlem2  27286  chirredlem3  27287  chirredlem4  27288  mdsymlem6  27303  cdj3lem2b  27332  esumpcvgval  28061  wfr3g  29317  frr3g  29361  nocvxmin  29426  heicant  30024  mblfinlem4  30029  ismblfin  30030  itg2addnc  30044  ftc1cnnc  30064  tailfb  30170  filbcmb  30206  prdsbnd  30264  ismtyval  30271  heiborlem8  30289  ghomco  30320  mzpindd  30653  mulltgt0  31351  stoweidlem46  31717  fourierdlem73  31851  usgvad2edg  32249  2zrngmmgm  32462  srhmsubc  32617  srhmsubcOLD  32636  zlmodzxzsubm  32681  zlmodzxzsub  32682  rp-fakenanass  37442
  Copyright terms: Public domain W3C validator