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

Theorem anc2li 542
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 21 . 2  |-  ( ph  ->  ph )
31, 2jctild 529 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  imdistani  673  equvini  2084  equviniOLD  2085  pwpw0  3948  sssn  3959  pwsnALT  4012  ordtr2  4627  tfis  4836  oeordi  6832  unblem3  7363  trcl  7666  h1datomi  23085  ballotlemfc0  24752  ballotlemfcc  24753  wfisg  25486  frinsg  25522  dfrdg4  25797  sbiota1  27613  equviniNEW7  29589
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 179  df-an 362
  Copyright terms: Public domain W3C validator