Theorem a2d 15

Description: Deduction distributing an embedded antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem a2d

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

Syntax hints:   → wi 2

This theorem is referenced by:  syl1 16  syl3d 26  mpdd 47  loowoz 67  pm3.43i 235  pm5.74 442  meredith 644  r19.20da 1255  dfwe2 2187  ordom 2382  findsg 2398  finds2 2399  tfindsg 2402  tfinds2 2405  tfinds3 2406  cleqfv 2880  funfvima2 2905  isofrlem 2939  tfr3 2964  tz7.48lem 2993  oaordi 3148  nnacl 3172  nnmcl 3173  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  nnmordi 3188  nneneq 3408  inf3lem2 3465  inf3lem5 3468  zornlem4 3606  zornlem5 3607  zornlem6 3608  zornlem7 3609  prlem934a 3931  suppsr3 4018  nnaddclt 4436  nnmulclt 4437  sup2 4510  uzind 4603  uzwo 4605  nnwoOLD 4608  om2uzlt 4654  seqrn 4673  expcllem 4682  expaddt 4698  occllem6 5185

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org