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

Theorem anc2li 555
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 525 1 (𝜑 → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  imdistani  568  pwpw0  4818  sssn  4831  wfisgOLD  6377  ordtr2  6430  tfis  7876  oeordi  8624  unblem3  9328  trcl  9766  frinsg  9789  clwlkclwwlkfo  30038  h1datomi  31610  ballotlemfc0  34474  ballotlemfcc  34475  pthisspthorcycl  35113  dfrdg4  35933  bj-sbsb  36820  bj-opelidres  37144  clsk1indlem3  44033  sbiota1  44430
  Copyright terms: Public domain W3C validator