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  4787  pwpw0  4836  ordtr2  6434  tfis  7900  oeordi  8634  unblem3  9324  trcl  9766  frinsg  9792  pthisspthorcycl  30447  clwlkclwwlkfo  30657  h1datomi  32240  ballotlemfc0  35236  ballotlemfcc  35237  kardcard2b  35974  dfrdg4  36930  bj-sbsb  37964  bj-opelidres  38350  clsk1indlem3  45304  sbiota1  45678