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

Theorem 3adantl3 1113
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 952 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 457 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  dif1enOLD  7106  dif1en  7107  infpssrlem4  7948  fin23lem11  7959  tskwun  8422  gruf  8449  lediv2a  9666  prunioo  10780  rpnnen2lem7  12515  muldvds1  12569  muldvds2  12570  dvdscmul  12571  dvdsmulc  12572  rpexp  12815  pospropd  14254  elcls  16826  cnpnei  17009  cnpflf2  17711  cnpflf  17712  cnpfcf  17752  xbln0  17981  blcls  18068  iimulcl  18451  icccvx  18464  iscau2  18719  cncombf  19029  mumul  20435  nvmul0or  21226  fh1  22213  fh2  22214  cm2j  22215  pjoi0  22312  hoadddi  22399  hmopco  22619  ax5seglem1  24628  ax5seglem2  24629  iscnp4  25666  ivthALT  26361  rngohomco  26708  rngoisoco  26716  ibliccsinexp  27848  iblioosinexp  27850  pexmidlem3N  30783  hdmapglem7  32744
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  df-3an 936
  Copyright terms: Public domain W3C validator