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  4817  sssn  4830  pwsnOLD  4902  wfisgOLD  6356  ordtr2  6409  tfis  7844  oeordi  8587  unblem3  9297  trcl  9723  frinsg  9746  clwlkclwwlkfo  29293  h1datomi  30865  ballotlemfc0  33522  ballotlemfcc  33523  pthisspthorcycl  34150  dfrdg4  34954  bj-sbsb  35763  bj-opelidres  36090  clsk1indlem3  42842  sbiota1  43241
  Copyright terms: Public domain W3C validator