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

Theorem anc2li 566
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 552 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  imdistani  704  pwpw0  4111  sssn  4122  pwsnALT  4185  wfisg  5422  ordtr2  5474  tfis  6700  oeordi  7306  unblem3  7843  trcl  8230  h1datomi  27315  ballotlemfc0  29398  ballotlemfcc  29399  frinsg  30554  dfrdg4  30789  bj-sbsb  31505  sbiota1  36855
  Copyright terms: Public domain W3C validator