Theorem anc2li 565

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 23	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	jctild 535	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imdistani  579  pwpw0  4774  sssn  4787  ordtr2  6408  tfis  7866  oeordi  8596  unblem3  9286  trcl  9729  frinsg  9755  pthisspthorcycl  30390  clwlkclwwlkfo  30600  h1datomi  32183  ballotlemfc0  35125  ballotlemfcc  35126  kardcard2b  35833  dfrdg4  36715  bj-sbsb  37749  bj-opelidres  38082  clsk1indlem3  45042  sbiota1  45417