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

Theorem 3adant2l 1222
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 1200 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1220 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1200 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  axdc3lem4  8834  modexp  12270  lmmbr2  21525  ax5seglem1  24004  ax5seglem2  24005  nvaddsub4  25329  pl1cn  27688  pellex  30602  fourierdlem42  31676  athgt  34469  ltrncoelN  35156  ltrncoat  35157  trlcoabs  35734  tendoplcl2  35791  tendopltp  35793  dih1dimatlem0  36342
  Copyright terms: Public domain W3C validator