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

Theorem anc2li 579
 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 565 1 (𝜑 → (𝜓 → (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  imdistani  725  pwpw0  4335  sssn  4349  pwsnALT  4420  wfisg  5703  ordtr2  5756  tfis  7039  oeordi  7652  unblem3  8199  trcl  8589  h1datomi  28410  ballotlemfc0  30528  ballotlemfcc  30529  frinsg  31716  dfrdg4  32033  bj-sbsb  32799  clsk1indlem3  38161  sbiota1  38455
 Copyright terms: Public domain W3C validator