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  4138  sssn  4148  pwsnALT  4203  ordtr2  4880  tfis  6598  oeordi  7160  unblem3  7701  trcl  8085  h1datomi  25453  ballotlemfc0  27331  ballotlemfcc  27332  wfisg  28126  frinsg  28162  dfrdg4  28437  sbiota1  30148
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