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

Theorem anc2li 557
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
Hypothesis
Ref Expression
anc2li.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
anc2li  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )

Proof of Theorem anc2li
StepHypRef Expression
1 anc2li.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 id 22 . 2  |-  ( ph  ->  ph )
31, 2jctild 543 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  imdistani  690  pwpw0  4159  sssn  4169  pwsnALT  4225  ordtr2  4908  tfis  6670  oeordi  7234  unblem3  7772  trcl  8157  h1datomi  26364  ballotlemfc0  28297  ballotlemfcc  28298  wfisg  29257  frinsg  29293  dfrdg4  29568  sbiota1  31288
  Copyright terms: Public domain W3C validator