Theorem anc2li 564

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 23	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	jctild 534	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imdistani  578  pwpw0  4783  sssn  4796  ordtr2  6407  tfis  7850  oeordi  8572  unblem3  9253  trcl  9696  frinsg  9722  pthisspthorcycl  30091  clwlkclwwlkfo  30300  h1datomi  31873  ballotlemfc0  34827  ballotlemfcc  34828  dfrdg4  36341  bj-sbsb  37360  bj-opelidres  37692  clsk1indlem3  44660  sbiota1  45035