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  5964  fvreseq0  5981  mpt2fun  6388  soxp  6896  oaass  7210  undifixp  7505  undom  7605  xpdom2  7612  tcrank  8302  inawinalem  9067  addcanpr  9424  ltsosr  9471  1re  9595  add42  9796  muladd  9989  mulsub  9999  divmuleq  10249  ltmul12a  10398  lemul12b  10399  lemul12a  10400  mulge0b  10412  qaddcl  11198  qmulcl  11200  iooshf  11603  fzass4  11721  elfzomelpfzo  11882  modid  11988  cshwleneq  12748  s2eq2seq  12845  tanaddlem  13762  fpwipodrs  15651  issubg4  16025  ghmpreima  16093  cntzsubg  16179  symgfixf1  16268  islmodd  17318  lssvsubcl  17390  lssvscl  17401  lmhmf1o  17492  pwsdiaglmhm  17503  lidlsubcl  17663  lmimco  18674  scmatghm  18830  scmatmhm  18831  mat2pmatscmxcl  19036  fctop  19299  cctop  19301  opnneissb  19409  pnrmopn  19638  hausnei2  19648  neitx  19871  txcnmpt  19888  txrest  19895  tx1stc  19914  fbssfi  20101  opnfbas  20106  rnelfmlem  20216  alexsubALTlem3  20312  metcnp3  20806  cncfmet  21175  evth  21222  caucfil  21485  ovolun  21673  dveflem  22143  efnnfsumcl  23132  efchtdvds  23189  lgsdir2  23359  axdimuniq  23920  axcontlem2  23972  friendship  24827  hvsub4  25658  his35  25709  shscli  25939  5oalem2  26277  3oalem2  26285  hosub4  26436  hmops  26643  hmopm  26644  hmopco  26646  adjmul  26715  adjadd  26716  mdslmd1lem1  26948  mdslmd1lem2  26949  dfon2lem6  28825  wfrlem4  28951  nofulllem4  29070  funline  29397  mbfposadd  29667  itg2addnc  29674  neibastop2lem  29809  fdc  29869  seqpo  29871  ismtyval  29927  mzpcompact2lem  30316  jm2.26  30576  zlmodzxzsubm  32044  paddss12  34633
  Copyright terms: Public domain W3C validator