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  4813  sssn  4826  wfisgOLD  6375  ordtr2  6428  tfis  7876  oeordi  8625  unblem3  9330  trcl  9768  frinsg  9791  pthisspthorcycl  29822  clwlkclwwlkfo  30028  h1datomi  31600  ballotlemfc0  34495  ballotlemfcc  34496  dfrdg4  35952  bj-sbsb  36838  bj-opelidres  37162  clsk1indlem3  44056  sbiota1  44453