Theorem anc2li 558

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 528	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imdistani  571  pwpw0  4748  sssn  4761  pwsnOLD  4833  wfisg  6185  ordtr2  6237  tfis  7571  oeordi  8215  unblem3  8774  trcl  9172  clwlkclwwlkfo  27789  h1datomi  29360  ballotlemfc0  31752  ballotlemfcc  31753  pthisspthorcycl  32377  frinsg  33089  dfrdg4  33414  bj-sbsb  34162  bj-opelidres  34455  clsk1indlem3  40400  sbiota1  40773