Theorem anc2li 555

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imdistani  568  pwpw0  4838  sssn  4851  wfisgOLD  6386  ordtr2  6439  tfis  7892  oeordi  8643  unblem3  9358  trcl  9797  frinsg  9820  clwlkclwwlkfo  30041  h1datomi  31613  ballotlemfc0  34457  ballotlemfcc  34458  pthisspthorcycl  35096  dfrdg4  35915  bj-sbsb  36803  bj-opelidres  37127  clsk1indlem3  44005  sbiota1  44403