Theorem anc2li 581

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

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  imdistani  728  pwpw0  4490  sssn  4504  pwsnALT  4582  wfisg  5877  ordtr2  5930  tfis  7221  oeordi  7839  unblem3  8382  trcl  8780  clwlkclwwlkfo  27154  h1datomi  28771  ballotlemfc0  30885  ballotlemfcc  30886  frinsg  32073  dfrdg4  32386  bj-sbsb  33153  clsk1indlem3  38862  sbiota1  39156