Theorem anc2li 559

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 529	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 210  df-an 400

This theorem is referenced by:  imdistani  572  pwpw0  4706  sssn  4719  pwsnOLD  4793  wfisg  6151  ordtr2  6203  tfis  7549  oeordi  8196  unblem3  8756  trcl  9154  clwlkclwwlkfo  27794  h1datomi  29364  ballotlemfc0  31860  ballotlemfcc  31861  pthisspthorcycl  32488  frinsg  33200  dfrdg4  33525  bj-sbsb  34275  bj-opelidres  34576  clsk1indlem3  40746  sbiota1  41138