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

Theorem 3adant2l 1179
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant2l  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )

Proof of Theorem 3adant2l
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com12 1158 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1177 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1158 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  axdc3lem4  8335  modexp  11516  lmmbr2  19214  nvaddsub4  22144  ax5seglem1  25869  ax5seglem2  25870  pellex  26900  athgt  30315  ltrncoelN  31002  ltrncoat  31003  trlcoabs  31580  tendoplcl2  31637  tendopltp  31639  dih1dimatlem0  32188
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator