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

Theorem ad2ant2l 727
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 697 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 695 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpteqb  5811  mpt2fun  6164  soxp  6451  oaass  6796  undifixp  7090  undom  7188  xpdom2  7195  tcrank  7800  inawinalem  8556  addcanpr  8915  ltsosr  8961  1re  9082  add42  9274  muladd  9458  mulsub  9468  divmuleq  9711  ltmul12a  9858  lemul12b  9859  lemul12a  9860  qaddcl  10582  qmulcl  10584  iooshf  10981  fzass4  11082  modid  11262  tanaddlem  12759  fpwipodrs  14582  issubg4  14953  ghmpreima  15019  cntzsubg  15127  islmodd  15948  lssvsubcl  16012  lssvscl  16023  lmhmf1o  16114  pwsdiaglmhm  16125  lidlsubcl  16279  fctop  17060  cctop  17062  opnneissb  17170  pnrmopn  17399  hausnei2  17409  neitx  17631  txcnmpt  17648  txrest  17655  tx1stc  17674  fbssfi  17861  opnfbas  17866  rnelfmlem  17976  alexsubALTlem3  18072  metcnp3  18562  cncfmet  18930  evth  18976  caucfil  19228  ovolun  19387  dveflem  19855  efnnfsumcl  20877  efchtdvds  20934  lgsdir2  21104  hvsub4  22531  his35  22582  shscli  22811  5oalem2  23149  3oalem2  23157  hosub4  23308  hmops  23515  hmopm  23516  hmopco  23518  adjmul  23587  adjadd  23588  mdslmd1lem1  23820  mdslmd1lem2  23821  mulge0b  25183  dfon2lem6  25407  wfrlem4  25533  nofulllem4  25652  axdimuniq  25844  axcontlem2  25896  funline  26068  mbfposadd  26244  itg2addnc  26249  neibastop2lem  26380  fdc  26440  seqpo  26442  ismtyval  26500  mzpcompact2lem  26799  jm2.26  27064  elfzomelpfzo  28112  paddss12  30553
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 178  df-an 361
  Copyright terms: Public domain W3C validator