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  7090  dif1en  7091  infpssrlem4  7932  fin23lem11  7943  tskwun  8406  gruf  8433  lediv2a  9650  prunioo  10764  rpnnen2lem7  12499  muldvds1  12553  muldvds2  12554  dvdscmul  12555  dvdsmulc  12556  rpexp  12799  pospropd  14238  elcls  16810  cnpnei  16993  cnpflf2  17695  cnpflf  17696  cnpfcf  17736  xbln0  17965  blcls  18052  iimulcl  18435  icccvx  18448  iscau2  18703  cncombf  19013  mumul  20419  nvmul0or  21210  fh1  22197  fh2  22198  cm2j  22199  pjoi0  22296  hoadddi  22383  hmopco  22603  ax5seglem1  24556  ax5seglem2  24557  iscnp4  25563  ivthALT  26258  rngohomco  26605  rngoisoco  26613  ibliccsinexp  27745  iblioosinexp  27747  pexmidlem3N  30161  hdmapglem7  32122
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