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

Theorem 3adantl1 1111
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
3adantl1  |-  ( ( ( ta  /\  ph  /\ 
ps )  /\  ch )  ->  th )

Proof of Theorem 3adantl1
StepHypRef Expression
1 3simpc 954 . 2  |-  ( ( ta  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 457 1  |-  ( ( ( ta  /\  ph  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2antl2  1118  3ad2antl3  1119  onfununi  6358  omord2  6565  en2eqpr  7637  divmuldiv  9460  ioojoin  10766  expnlbnd  11231  pospropd  14238  upxp  17317  rnelfmlem  17647  fh2  22198  homulass  22382  hoadddi  22383  hoadddir  22384  brbtwn2  24533  metf1o  26469  rngohomco  26605  rngoisoco  26613  paddss12  30008
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