Theorem anc2li 557

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  imdistani  570  pwpw0  4817  sssn  4830  pwsnOLD  4902  wfisgOLD  6356  ordtr2  6409  tfis  7844  oeordi  8587  unblem3  9297  trcl  9723  frinsg  9746  clwlkclwwlkfo  29262  h1datomi  30834  ballotlemfc0  33491  ballotlemfcc  33492  pthisspthorcycl  34119  dfrdg4  34923  bj-sbsb  35715  bj-opelidres  36042  clsk1indlem3  42794  sbiota1  43193