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

Theorem anc2li 557
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 527 1 (𝜑 → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  imdistani  570  pwpw0  4777  sssn  4790  pwsnOLD  4862  wfisgOLD  6312  ordtr2  6365  tfis  7795  oeordi  8538  unblem3  9247  trcl  9672  frinsg  9695  clwlkclwwlkfo  29002  h1datomi  30572  ballotlemfc0  33156  ballotlemfcc  33157  pthisspthorcycl  33786  dfrdg4  34589  bj-sbsb  35355  bj-opelidres  35682  clsk1indlem3  42407  sbiota1  42806
  Copyright terms: Public domain W3C validator