MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anc2li Unicode 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 543 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  imdistani  690  pwpw0  4178  sssn  4188  pwsnALT  4244  ordtr2  4927  tfis  6689  oeordi  7255  unblem3  7794  trcl  8180  h1datomi  26499  ballotlemfc0  28431  ballotlemfcc  28432  wfisg  29289  frinsg  29325  dfrdg4  29600  sbiota1  31341
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 185  df-an 371
  Copyright terms: Public domain W3C validator