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

Theorem anc2li 540
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 19 . 2  |-  ( ph  ->  ph )
31, 2jctild 527 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imdistani  671  equvini  1927  pwpw0  3763  sssn  3772  pwsnALT  3822  ordtr2  4436  tfis  4645  oeordi  6585  unblem3  7111  trcl  7410  h1datomi  22160  ballotlemfc0  23051  ballotlemfcc  23052  wfisg  24209  frinsg  24245  dfrdg4  24488  setiscat  25979  sbiota1  27634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator