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  5576  mpt2fun  5908  soxp  6190  oaass  6555  undifixp  6848  undom  6946  xpdom2  6953  tcrank  7550  inawinalem  8307  addcanpr  8666  ltsosr  8712  1re  8833  add42  9024  muladd  9208  mulsub  9218  divmuleq  9461  ltmul12a  9608  lemul12b  9609  lemul12a  9610  qaddcl  10328  qmulcl  10330  iooshf  10724  fzass4  10825  modid  10989  tanaddlem  12442  fpwipodrs  14263  issubg4  14634  ghmpreima  14700  cntzsubg  14808  islmodd  15629  lssvsubcl  15697  lssvscl  15708  lmhmf1o  15799  pwsdiaglmhm  15810  lidlsubcl  15964  fctop  16737  cctop  16739  opnneissb  16847  pnrmopn  17067  hausnei2  17077  txcnmpt  17314  txrest  17321  tx1stc  17340  fbssfi  17528  opnfbas  17533  rnelfmlem  17643  alexsubALTlem3  17739  metcnp3  18082  cncfmet  18408  evth  18453  caucfil  18705  ovolun  18854  dveflem  19322  efnnfsumcl  20336  efchtdvds  20393  lgsdir2  20563  hvsub4  21612  his35  21663  shscli  21892  5oalem2  22230  3oalem2  22238  hosub4  22389  hmops  22596  hmopm  22597  hmopco  22599  adjmul  22668  adjadd  22669  mdslmd1lem1  22901  mdslmd1lem2  22902  mulge0b  23492  dfon2lem6  23548  wfrlem4  23663  axfelem10  23759  axfelem14  23763  axfelem18  23767  axdimuniq  23951  axcontlem2  24003  funline  24175  cbcpcp  24573  prdnei  24984  limptlimpr2lem2  24986  neibastop2lem  25720  fdc  25866  seqpo  25868  ismtyval  25935  mzpcompact2lem  26240  jm2.26  26506  paddss12  29287
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