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

Theorem anc2li 581
 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 567 1 (𝜑 → (𝜓 → (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  imdistani  728  pwpw0  4490  sssn  4504  pwsnALT  4582  wfisg  5877  ordtr2  5930  tfis  7221  oeordi  7839  unblem3  8382  trcl  8780  clwlkclwwlkfo  27154  h1datomi  28771  ballotlemfc0  30885  ballotlemfcc  30886  frinsg  32073  dfrdg4  32386  bj-sbsb  33153  clsk1indlem3  38862  sbiota1  39156
 Copyright terms: Public domain W3C validator