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  4779  sssn  4792  ordtr2  6406  tfis  7847  oeordi  8569  unblem3  9250  trcl  9693  frinsg  9719  pthisspthorcycl  30151  clwlkclwwlkfo  30360  h1datomi  31933  ballotlemfc0  34883  ballotlemfcc  34884  kardcard2b  35578  dfrdg4  36443  bj-sbsb  37472  bj-opelidres  37805  clsk1indlem3  44769  sbiota1  45144