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  6374  omord2  6581  en2eqpr  7653  divmuldiv  9476  ioojoin  10782  expnlbnd  11247  pospropd  14254  upxp  17333  rnelfmlem  17663  fh2  22214  homulass  22398  hoadddi  22399  hoadddir  22400  brbtwn2  24605  metf1o  26572  rngohomco  26708  rngoisoco  26716  paddss12  30630
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