Theorem anc2li 560

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 530	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 208  df-an 397

This theorem is referenced by:  imdistani  573  pwpw0  4744  sssn  4757  ordtr2  6355  tfis  7795  oeordi  8513  unblem3  9194  trcl  9640  frinsg  9666  pthisspthorcycl  29888  clwlkclwwlkfo  30097  h1datomi  31670  ballotlemfc0  34677  ballotlemfcc  34678  dfrdg4  36179  bj-sbsb  37190  bj-opelidres  37521  clsk1indlem3  44487  sbiota1  44878