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

Theorem 3adant2l 1258
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 1209 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1256 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1209 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  axdc3lem4  8872  modexp  12393  lmmbr2  22148  ax5seglem1  24845  ax5seglem2  24846  nvaddsub4  26168  pl1cn  28641  athgt  32774  ltrncoelN  33461  ltrncoat  33462  trlcoabs  34041  tendoplcl2  34098  tendopltp  34100  dih1dimatlem0  34649  pellex  35433  fourierdlem42  37628
  Copyright terms: Public domain W3C validator