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  6403  tfis  7852  oeordi  8576  unblem3  9265  trcl  9708  frinsg  9734  pthisspthorcycl  30270  clwlkclwwlkfo  30480  h1datomi  32063  ballotlemfc0  35005  ballotlemfcc  35006  kardcard2b  35692  dfrdg4  36531  bj-sbsb  37581  bj-opelidres  37914  clsk1indlem3  44884  sbiota1  45259