Theorem a2d 23

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (φ → (ψ → (χ → θ)))

Assertion

Ref	Expression
a2d	⊢ (φ → ((ψ → χ) → (ψ → θ)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (φ → (ψ → (χ → θ)))
2		ax-2 6	. 2 ⊢ ((ψ → (χ → θ)) → ((ψ → χ) → (ψ → θ)))
3	1, 2	syl 14	1 ⊢ (φ → ((ψ → χ) → (ψ → θ)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mpdd  36  imim2d  48  imim3i  55  loowoz  96  cbv1  1629  ralimdaa  2380  reuss2  3211  finds2  4267  ssrel  4371  ssrel2  4373  ssrelrel  4383  funfvima2  5334  tfrlem1  5864  tfrlemi1  5887  tfri3  5894  rdgon  5913  pitonn  6744  nnaddcl  7715  nnmulcl  7716  zaddcllempos  8058  zaddcllemneg  8060  peano5uzti  8122  uzind2  8126  fzind  8129  zindd  8132  uzaddcl  8305  frec2uzltd  8870  iseqfveq2  8905  expivallem  8910  expcllem  8920  expap0  8939  mulexp  8948  expadd  8951  expmul  8954  leexp2r  8962  leexp1a  8963  bernneq  9022  cjexp  9121