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

Theorem 3adantl3 1115
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3adantl3  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 954 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  dif1enOLD  7307  dif1en  7308  infpssrlem4  8150  fin23lem11  8161  tskwun  8623  gruf  8650  lediv2a  9868  prunioo  10989  rpnnen2lem7  12783  muldvds1  12837  muldvds2  12838  dvdscmul  12839  dvdsmulc  12840  rpexp  13083  pospropd  14524  elcls  17100  iscnp4  17289  cnpnei  17290  cnpflf2  17993  cnpflf  17994  cnpfcf  18034  xbln0  18405  blcls  18497  iimulcl  18923  icccvx  18936  iscau2  19191  cncombf  19511  mumul  20925  nvmul0or  22094  fh1  23081  fh2  23082  cm2j  23083  pjoi0  23180  hoadddi  23267  hmopco  23487  iocinif  24105  volfiniune  24547  ax5seglem1  25779  ax5seglem2  25780  cnambfre  26162  ivthALT  26236  rngohomco  26488  rngoisoco  26496  ibliccsinexp  27620  iblioosinexp  27622  pexmidlem3N  30466  hdmapglem7  32427
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  df-3an 938
  Copyright terms: Public domain W3C validator