Theorem anc2li 555

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 525	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  imdistani  568  pwpw0  4812  sssn  4825  wfisgOLD  6354  ordtr2  6407  tfis  7853  oeordi  8601  unblem3  9315  trcl  9745  frinsg  9768  clwlkclwwlkfo  29812  h1datomi  31384  ballotlemfc0  34106  ballotlemfcc  34107  pthisspthorcycl  34732  dfrdg4  35541  bj-sbsb  36308  bj-opelidres  36634  clsk1indlem3  43467  sbiota1  43865