Theorem a2d 26

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  40  imim2d  53  imim3i  60  loowoz  101  cbv1  1672  ralimdaa  2428  reuss2  3244  finds2  4342  ssrel  4446  ssrel2  4448  ssrelrel  4458  funfvima2  5412  tfrlem1  5946  tfrlemi1  5969  tfri3  5976  rdgon  5996  nneneq  6343  ac6sfi  6379  pitonn  7016  nnaddcl  8059  nnmulcl  8060  zaddcllempos  8388  zaddcllemneg  8390  peano5uzti  8455  uzind2  8459  fzind  8462  zindd  8465  uzaddcl  8674  exfzdc  9249  frec2uzltd  9405  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqhomo  9468  iseqz  9469  expivallem  9477  expcllem  9487  expap0  9506  mulexp  9515  expadd  9518  expmul  9521  leexp2r  9530  leexp1a  9531  bernneq  9593  facdiv  9665  facwordi  9667  faclbnd  9668  faclbnd6  9671  cjexp  9780  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  absexp  9965  dvdsfac  10260  gcdmultiple  10409  rplpwr  10416  nn0seqcvgd  10423  ialginv  10429  ialgcvga  10433  ialgfx  10434  prmdvdsexp  10527  prmfac1  10531