Theorem anc2li 559

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 23	. 2 |- ( ph -> ph )
3	1, 2	jctild 545	1 |- ( ph -> ( ps -> ( ph /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  imdistani  694  pwpw0  4145  sssn  4155  pwsnALT  4211  wfisg  5430  ordtr2  5482  tfis  6691  oeordi  7292  unblem3  7827  trcl  8213  h1datomi  27217  ballotlemfc0  29318  ballotlemfcc  29319  frinsg  30475  dfrdg4  30708  sbiota1  36640