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

Theorem anc2li 558
 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 528 1 (𝜑 → (𝜓 → (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  imdistani  571  pwpw0  4738  sssn  4751  pwsnALT  4823  wfisg  6176  ordtr2  6228  tfis  7561  oeordi  8205  unblem3  8764  trcl  9162  clwlkclwwlkfo  27779  h1datomi  29350  ballotlemfc0  31738  ballotlemfcc  31739  pthisspthorcycl  32363  frinsg  33075  dfrdg4  33400  bj-sbsb  34148  bj-opelidres  34440  clsk1indlem3  40378  sbiota1  40751
 Copyright terms: Public domain W3C validator