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

Theorem ad2ant2r 739
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 709 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 707 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  5618  fvreseq0  5791  fliftfun  5992  omordi  6993  f1imaen2g  7358  isinf  7514  frfi  7545  acndom2  8212  infxp  8372  cff1  8415  isf32lem7  8516  fpwwe2lem12  8796  inawinalem  8844  inar1  8930  grur1  8975  genpnnp  9162  ltexprlem7  9199  prlem936  9204  reclem3pr  9206  1re  9373  addsub4  9640  muladd  9765  lt2add  9812  mullt0  9847  mulnzcnopr  9970  divmuldiv  10019  divmul24  10023  divmuleq  10024  recdiv  10025  divadddiv  10034  conjmul  10036  prodgt0  10162  ltmul12a  10173  lemul12b  10174  lediv12a  10213  lediv2a  10214  qmulcl  10959  irrmul  10966  xrrege0  11134  xmulge0  11235  ge0addcl  11384  ge0mulcl  11385  ge0xaddcl  11386  ge0xmulcl  11387  fzass4  11483  fzrev  11503  fzm1  11524  serge0  11844  expclzlem  11873  expge0  11884  expge1  11885  lt2sq  11923  le2sq  11924  bernneq  11974  wrdeqswrdlsw  12327  cshwleneq  12435  s2eq2seq  12528  sqrmo  12725  limsupval2  12942  o1lo12  13000  climrlim2  13009  2clim  13034  climsup  13131  tanaddlem  13433  divalglem8  13587  opeo  13863  omeo  13864  pcpremul  13893  pcmul  13901  setscom  14187  fpwipodrs  15317  grplactcnv  15604  resgrpisgrp  15682  ghmpreima  15748  ghmeql  15749  conjghm  15757  pgpfi  16084  lmodprop2d  16931  lidlmcl  17221  xrs1mnd  17695  absabv  17714  lmimco  18115  mavmulass  18202  cramerimplem2  18332  opnneissb  18560  cncnpi  18724  pnrmopn  18789  cmpsub  18845  connsub  18867  t1conperf  18882  neitx  19022  txcnmpt  19039  txrest  19046  txdis1cn  19050  tx1stc  19065  qtopcn  19129  trfg  19306  rnelfmlem  19367  flffbas  19410  nmo0  20156  nmoid  20163  cfilfcls  20627  iscmet3lem2  20645  caubl  20660  relcmpcmet  20669  ovolun  20824  ovolicc2lem3  20844  volsup  20879  ioombl1lem4  20884  ismbf3d  20974  mbfimaopnlem  20975  i1faddlem  21013  itgle  21129  ellimc2  21194  ftc1a  21351  dgrmul  21622  itgulm  21758  abelthlem8  21789  ptolemy  21843  logdivlt  21955  cxplt3  22030  cxple3  22031  o1cxp  22253  basellem4  22306  sqf11  22362  lgslem3  22522  lgsdir2  22552  lgsne0  22557  lgsquad3  22585  chpo1ubb  22615  vmadivsumb  22617  rpvmasumlem  22621  dchrisum0re  22647  dchrisum0  22654  selberg2b  22686  selberg3lem2  22692  pntrsumbnd  22700  pntrlog2bnd  22718  axcontlem2  23034  grporcan  23531  isgrp2d  23545  ablomul  23665  blocni  24028  ubthlem3  24096  htthlem  24142  hvsub4  24262  shscli  24543  elspansn4  24799  5oalem2  24881  hosub4  25040  hmops  25247  hmopco  25250  adjadd  25320  hstpyth  25456  hstles  25458  mdsl0  25537  mdslmd1lem2  25553  chirredlem1  25617  chirredlem2  25618  chirredlem3  25619  chirredlem4  25620  mdsymlem6  25635  cdj3lem2b  25664  resf1o  25855  esumpcvgval  26381  wfr3g  27570  frr3g  27614  nocvxmin  27679  heicant  28270  mblfinlem4  28275  ismblfin  28276  itg2addnc  28290  ftc1cnnc  28310  reftr  28405  tailfb  28442  filbcmb  28478  prdsbnd  28536  ismtyval  28543  heiborlem8  28561  ghomco  28592  mzpindd  28927  mulltgt0  29589  stoweidlem46  29687  2wlkeq  30134  usgra2adedgspth  30151  wwlkext2clwwlk  30311  zlmodzxzsubm  30590  zlmodzxzsub  30591
  Copyright terms: Public domain W3C validator