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  4168  sssn  4178  pwsnALT  4233  ordtr2  4915  tfis  6660  oeordi  7226  unblem3  7763  trcl  8148  h1datomi  26025  ballotlemfc0  27921  ballotlemfcc  27922  wfisg  28716  frinsg  28752  dfrdg4  29027  sbiota1  30738