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  4767  sssn  4780  ordtr2  6360  tfis  7795  oeordi  8513  unblem3  9192  trcl  9635  frinsg  9661  pthisspthorcycl  29824  clwlkclwwlkfo  30033  h1datomi  31605  ballotlemfc0  34599  ballotlemfcc  34600  dfrdg4  36094  bj-sbsb  36981  bj-opelidres  37305  clsk1indlem3  44226  sbiota1  44617