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

Theorem 3adant2l 1212
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 1191 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1l 1210 . 2  |-  ( ( ( ta  /\  ps )  /\  ph  /\  ch )  ->  th )
433com12 1191 1  |-  ( (
ph  /\  ( ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  axdc3lem4  8634  modexp  12011  lmmbr2  20782  ax5seglem1  23186  ax5seglem2  23187  nvaddsub4  24053  pl1cn  26397  pellex  29188  athgt  33112  ltrncoelN  33799  ltrncoat  33800  trlcoabs  34377  tendoplcl2  34434  tendopltp  34436  dih1dimatlem0  34985
  Copyright terms: Public domain W3C validator