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

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

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrl 715 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 713 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  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:  mpteqb  5786  fvreseq0  5801  mpt2fun  6190  soxp  6683  oaass  6998  undifixp  7297  undom  7397  xpdom2  7404  tcrank  8089  inawinalem  8854  addcanpr  9213  ltsosr  9259  1re  9383  add42  9584  muladd  9775  mulsub  9785  divmuleq  10034  ltmul12a  10183  lemul12b  10184  lemul12a  10185  mulge0b  10197  qaddcl  10967  qmulcl  10969  iooshf  11372  fzass4  11494  elfzomelpfzo  11627  modid  11730  cshwleneq  12449  s2eq2seq  12542  tanaddlem  13448  fpwipodrs  15332  issubg4  15698  ghmpreima  15766  cntzsubg  15852  symgfixf1  15941  islmodd  16952  lssvsubcl  17023  lssvscl  17034  lmhmf1o  17125  pwsdiaglmhm  17136  lidlsubcl  17296  lmimco  18271  fctop  18606  cctop  18608  opnneissb  18716  pnrmopn  18945  hausnei2  18955  neitx  19178  txcnmpt  19195  txrest  19202  tx1stc  19221  fbssfi  19408  opnfbas  19413  rnelfmlem  19523  alexsubALTlem3  19619  metcnp3  20113  cncfmet  20482  evth  20529  caucfil  20792  ovolun  20980  dveflem  21449  efnnfsumcl  22438  efchtdvds  22495  lgsdir2  22665  axdimuniq  23157  axcontlem2  23209  hvsub4  24437  his35  24488  shscli  24718  5oalem2  25056  3oalem2  25064  hosub4  25215  hmops  25422  hmopm  25423  hmopco  25425  adjmul  25494  adjadd  25495  mdslmd1lem1  25727  mdslmd1lem2  25728  dfon2lem6  27599  wfrlem4  27725  nofulllem4  27844  funline  28171  mbfposadd  28436  itg2addnc  28443  neibastop2lem  28578  fdc  28638  seqpo  28640  ismtyval  28696  mzpcompact2lem  29085  jm2.26  29348  friendship  30712  zlmodzxzsubm  30753  paddss12  33460
  Copyright terms: Public domain W3C validator