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

Theorem 3adant2l 1178
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 1157 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1176 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1157 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  axdc3lem4  8297  modexp  11477  lmmbr2  19173  nvaddsub4  22103  ax5seglem1  25779  ax5seglem2  25780  pellex  26796  athgt  29950  ltrncoelN  30637  ltrncoat  30638  trlcoabs  31215  tendoplcl2  31272  tendopltp  31274  dih1dimatlem0  31823
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