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  1940  pwpw0  3779  sssn  3788  pwsnALT  3838  ordtr2  4452  tfis  4661  oeordi  6601  unblem3  7127  trcl  7426  h1datomi  22176  ballotlemfc0  23067  ballotlemfcc  23068  wfisg  24280  frinsg  24316  dfrdg4  24560  setiscat  26082  sbiota1  27737  equviniNEW7  29502
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