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  6257  ordtr2  6310  tfis  7701  oeordi  8418  unblem3  9068  trcl  9486  frinsg  9509  clwlkclwwlkfo  28373  h1datomi  29943  ballotlemfc0  32459  ballotlemfcc  32460  pthisspthorcycl  33090  dfrdg4  34253  bj-sbsb  35020  bj-opelidres  35332  clsk1indlem3  41653  sbiota1  42052