Theorem anc2li 556

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  imdistani  569  pwpw0  4746  sssn  4759  pwsnOLD  4832  wfisgOLD  6250  ordtr2  6303  tfis  7691  oeordi  8405  unblem3  9055  trcl  9495  frinsg  9519  clwlkclwwlkfo  28381  h1datomi  29951  ballotlemfc0  32467  ballotlemfcc  32468  pthisspthorcycl  33098  dfrdg4  34261  bj-sbsb  35028  bj-opelidres  35340  clsk1indlem3  41634  sbiota1  42033