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  4168  sssn  4178  pwsnALT  4233  ordtr2  4915  tfis  6660  oeordi  7226  unblem3  7763  trcl  8148  h1datomi  26025  ballotlemfc0  27921  ballotlemfcc  27922  wfisg  28716  frinsg  28752  dfrdg4  29027  sbiota1  30738
  Copyright terms: Public domain W3C validator