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

Theorem 3adant2l 1176
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 1155 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1174 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1155 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  axdc3lem4  8095  modexp  11252  lmmbr2  18701  nvaddsub4  21235  ax5seglem1  24628  ax5seglem2  24629  pellex  27023  athgt  30267  ltrncoelN  30954  ltrncoat  30955  trlcoabs  31532  tendoplcl2  31589  tendopltp  31591  dih1dimatlem0  32140
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