MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2ant2l 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  5759  mpt2fun  6112  soxp  6396  oaass  6741  undifixp  7035  undom  7133  xpdom2  7140  tcrank  7742  inawinalem  8498  addcanpr  8857  ltsosr  8903  1re  9024  add42  9215  muladd  9399  mulsub  9409  divmuleq  9652  ltmul12a  9799  lemul12b  9800  lemul12a  9801  qaddcl  10523  qmulcl  10525  iooshf  10922  fzass4  11023  modid  11198  tanaddlem  12695  fpwipodrs  14518  issubg4  14889  ghmpreima  14955  cntzsubg  15063  islmodd  15884  lssvsubcl  15948  lssvscl  15959  lmhmf1o  16050  pwsdiaglmhm  16061  lidlsubcl  16215  fctop  16992  cctop  16994  opnneissb  17102  pnrmopn  17330  hausnei2  17340  neitx  17561  txcnmpt  17578  txrest  17585  tx1stc  17604  fbssfi  17791  opnfbas  17796  rnelfmlem  17906  alexsubALTlem3  18002  metcnp3  18461  cncfmet  18810  evth  18856  caucfil  19108  ovolun  19263  dveflem  19731  efnnfsumcl  20753  efchtdvds  20810  lgsdir2  20980  hvsub4  22388  his35  22439  shscli  22668  5oalem2  23006  3oalem2  23014  hosub4  23165  hmops  23372  hmopm  23373  hmopco  23375  adjmul  23444  adjadd  23445  mdslmd1lem1  23677  mdslmd1lem2  23678  mulge0b  24971  dfon2lem6  25169  wfrlem4  25284  nofulllem4  25384  axdimuniq  25567  axcontlem2  25619  funline  25791  neibastop2lem  26081  fdc  26141  seqpo  26143  ismtyval  26201  mzpcompact2lem  26500  jm2.26  26765  paddss12  29934
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