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

Theorem anc2li 559
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 23 . 2  |-  ( ph  ->  ph )
31, 2jctild 545 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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
This theorem is referenced by:  imdistani  694  pwpw0  4145  sssn  4155  pwsnALT  4211  wfisg  5430  ordtr2  5482  tfis  6691  oeordi  7292  unblem3  7827  trcl  8213  h1datomi  27217  ballotlemfc0  29318  ballotlemfcc  29319  frinsg  30475  dfrdg4  30708  sbiota1  36640
  Copyright terms: Public domain W3C validator