Theorem anc2li 566

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 552	1 |- ( ph -> ( ps -> ( ph /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  imdistani  704  pwpw0  4111  sssn  4122  pwsnALT  4185  wfisg  5422  ordtr2  5474  tfis  6700  oeordi  7306  unblem3  7843  trcl  8230  h1datomi  27315  ballotlemfc0  29398  ballotlemfcc  29399  frinsg  30554  dfrdg4  30789  bj-sbsb  31505  sbiota1  36855