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  4781  sssn  4794  ordtr2  6410  tfis  7857  oeordi  8579  unblem3  9261  trcl  9704  frinsg  9730  pthisspthorcycl  30217  clwlkclwwlkfo  30427  h1datomi  32004  ballotlemfc0  34948  ballotlemfcc  34949  kardcard2b  35635  dfrdg4  36480  bj-sbsb  37529  bj-opelidres  37862  clsk1indlem3  44827  sbiota1  45202