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  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