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  6704  nnaddcl  7675  nnmulcl  7676  zaddcllempos  8018  zaddcllemneg  8020  peano5uzti  8082  uzind2  8086  fzind  8089  zindd  8092  uzaddcl  8265  frec2uzltd  8830  iseqfveq2  8865  expivallem  8870  expcllem  8880  expap0  8899  mulexp  8908  expadd  8911  expmul  8914  leexp2r  8922  leexp1a  8923  bernneq  8982  cjexp  9081