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

Step	Hyp	Ref	Expression
1		anc2li.1	. 2
2		id 22	. 2
3	1, 2	jctild 543	1

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