Theorem anc2li 563

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 533	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imdistani  576  pwpw0  4771  sssn  4784  ordtr2  6391  tfis  7835  oeordi  8557  unblem3  9238  trcl  9683  frinsg  9709  pthisspthorcycl  29999  clwlkclwwlkfo  30208  h1datomi  31781  ballotlemfc0  34787  ballotlemfcc  34788  dfrdg4  36298  bj-sbsb  37319  bj-opelidres  37650  clsk1indlem3  44616  sbiota1  45007