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

Theorem anc2li 552
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
anc2li (𝜑 → (𝜓 → (𝜑𝜒)))

Proof of Theorem anc2li
StepHypRef Expression
1 anc2li.1 . 2 (𝜑 → (𝜓𝜒))
2 id 22 . 2 (𝜑𝜑)
31, 2jctild 522 1 (𝜑 → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  imdistani  565  pwpw0  4530  sssn  4543  pwsnALT  4619  wfisg  5931  ordtr2  5983  tfis  7286  oeordi  7905  unblem3  8454  trcl  8852  clwlkclwwlkfoOLD  27298  clwlkclwwlkfo  27302  h1datomi  28957  ballotlemfc0  31063  ballotlemfcc  31064  frinsg  32250  dfrdg4  32563  bj-sbsb  33311  clsk1indlem3  39111  sbiota1  39404
  Copyright terms: Public domain W3C validator