Theorem anc2li 558

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imdistani  571  pwpw0  4739  sssn  4752  pwsnALT  4824  wfisg  6177  ordtr2  6229  tfis  7563  oeordi  8207  unblem3  8766  trcl  9164  clwlkclwwlkfo  27781  h1datomi  29352  ballotlemfc0  31745  ballotlemfcc  31746  pthisspthorcycl  32370  frinsg  33082  dfrdg4  33407  bj-sbsb  34155  bj-opelidres  34447  clsk1indlem3  40386  sbiota1  40759