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  4816  sssn  4829  pwsnOLD  4901  wfisgOLD  6355  ordtr2  6408  tfis  7843  oeordi  8586  unblem3  9296  trcl  9722  frinsg  9745  clwlkclwwlkfo  29259  h1datomi  30829  ballotlemfc0  33486  ballotlemfcc  33487  pthisspthorcycl  34114  dfrdg4  34918  bj-sbsb  35710  bj-opelidres  36037  clsk1indlem3  42784  sbiota1  43183