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

Theorem ad2ant2l 726
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 696 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 694 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpteqb  5614  mpt2fun  5946  soxp  6228  oaass  6559  undifixp  6852  undom  6950  xpdom2  6957  tcrank  7554  inawinalem  8311  addcanpr  8670  ltsosr  8716  1re  8837  add42  9028  muladd  9212  mulsub  9222  divmuleq  9465  ltmul12a  9612  lemul12b  9613  lemul12a  9614  qaddcl  10332  qmulcl  10334  iooshf  10728  fzass4  10829  modid  10993  tanaddlem  12446  fpwipodrs  14267  issubg4  14638  ghmpreima  14704  cntzsubg  14812  islmodd  15633  lssvsubcl  15701  lssvscl  15712  lmhmf1o  15803  pwsdiaglmhm  15814  lidlsubcl  15968  fctop  16741  cctop  16743  opnneissb  16851  pnrmopn  17071  hausnei2  17081  txcnmpt  17318  txrest  17325  tx1stc  17344  fbssfi  17532  opnfbas  17537  rnelfmlem  17647  alexsubALTlem3  17743  metcnp3  18086  cncfmet  18412  evth  18457  caucfil  18709  ovolun  18858  dveflem  19326  efnnfsumcl  20340  efchtdvds  20397  lgsdir2  20567  hvsub4  21616  his35  21667  shscli  21896  5oalem2  22234  3oalem2  22242  hosub4  22393  hmops  22600  hmopm  22601  hmopco  22603  adjmul  22672  adjadd  22673  mdslmd1lem1  22905  mdslmd1lem2  22906  mulge0b  24086  dfon2lem6  24144  wfrlem4  24259  nofulllem4  24359  axdimuniq  24541  axcontlem2  24593  funline  24765  cbcpcp  25162  prdnei  25573  limptlimpr2lem2  25575  neibastop2lem  26309  fdc  26455  seqpo  26457  ismtyval  26524  mzpcompact2lem  26829  jm2.26  27095  paddss12  30008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator