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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
anc2li	|- ( ph -> ( ps -> ( ph /\ ch ) ) )

Proof of Theorem anc2li

Step	Hyp	Ref	Expression
1		anc2li.1	. 2 |- ( ph -> ( ps -> ch ) )
2		id 22	. 2 |- ( ph -> ph )
3	1, 2	jctild 543	1 |- ( ph -> ( ps -> ( ph /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  imdistani  690  pwpw0  4159  sssn  4169  pwsnALT  4225  ordtr2  4908  tfis  6670  oeordi  7234  unblem3  7772  trcl  8157  h1datomi  26364  ballotlemfc0  28297  ballotlemfcc  28298  wfisg  29257  frinsg  29293  dfrdg4  29568  sbiota1  31288