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

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

Proof of Theorem 3adantl1
StepHypRef Expression
1 3simpc 956 . 2  |-  ( ( ta  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ta  /\  ph  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ad2antl2  1120  3ad2antl3  1121  onfununi  6603  omord2  6810  en2eqpr  7891  divmuldiv  9714  ioojoin  11027  expnlbnd  11509  pospropd  14561  upxp  17655  rnelfmlem  17984  fh2  23121  homulass  23305  hoadddi  23306  hoadddir  23307  brbtwn2  25844  metf1o  26461  rngohomco  26590  rngoisoco  26598  swrdltnd  28181  paddss12  30616
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