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  4756  sssn  4769  ordtr2  6368  tfis  7806  oeordi  8523  unblem3  9204  trcl  9649  frinsg  9675  pthisspthorcycl  29870  clwlkclwwlkfo  30079  h1datomi  31652  ballotlemfc0  34637  ballotlemfcc  34638  dfrdg4  36133  bj-sbsb  37144  bj-opelidres  37475  clsk1indlem3  44470  sbiota1  44861