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

This theorem is referenced by:  imdistani  568  pwpw0  4743  sssn  4756  pwsnOLD  4829  wfisgOLD  6242  ordtr2  6295  tfis  7676  oeordi  8380  unblem3  8998  trcl  9417  frinsg  9440  clwlkclwwlkfo  28274  h1datomi  29844  ballotlemfc0  32359  ballotlemfcc  32360  pthisspthorcycl  32990  dfrdg4  34180  bj-sbsb  34947  bj-opelidres  35259  clsk1indlem3  41542  sbiota1  41941