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  sssn  4781  pwpw0  4830  ordtr2  6411  tfis  7870  oeordi  8604  unblem3  9294  trcl  9736  frinsg  9762  pthisspthorcycl  30399  clwlkclwwlkfo  30609  h1datomi  32192  ballotlemfc0  35175  ballotlemfcc  35176  kardcard2b  35901  dfrdg4  36839  bj-sbsb  37873  bj-opelidres  38219  clsk1indlem3  45180  sbiota1  45554