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 7	. 2 ⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
3	1, 2	syl 14	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Syntax hints:   → wi 4

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

This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  102  animpimp2impd  548  cbv1  1722  ralimdaa  2496  reuss2  3351  finds2  4510  ssrel  4622  ssrel2  4624  ssrelrel  4634  funfvima2  5643  tfrlem1  6198  tfrlemi1  6222  tfr1onlemaccex  6238  tfrcllemaccex  6251  tfri3  6257  nneneq  6744  ac6sfi  6785  pitonn  7649  nnaddcl  8733  nnmulcl  8734  zaddcllempos  9084  zaddcllemneg  9086  peano5uzti  9152  uzind2  9156  fzind  9159  zindd  9162  uzaddcl  9374  exfzdc  10010  frec2uzltd  10169  frecuzrdgg  10182  seq3val  10224  seqvalcd  10225  seq3clss  10233  monoord  10242  seq3caopr3  10247  seq3f1olemp  10268  seq3id3  10273  seq3homo  10276  seq3z  10277  ser3ge0  10283  exp3vallem  10287  expcllem  10297  expap0  10316  mulexp  10325  expadd  10328  expmul  10331  leexp2r  10340  leexp1a  10341  bernneq  10405  facdiv  10477  facwordi  10479  faclbnd  10480  faclbnd6  10483  omgadd  10541  seq3coll  10578  cjexp  10658  resqrexlemover  10775  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc3  10781  absexp  10844  fsum2d  11197  modfsummod  11220  fsumabs  11227  fsumiun  11239  binom  11246  bcxmas  11251  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  clim2prod  11301  prodfap0  11307  prodfrecap  11308  demoivreALT  11469  dvdsfac  11547  gcdmultiple  11697  rplpwr  11704  nn0seqcvgd  11711  alginv  11717  algcvga  11721  algfx  11722  prmdvdsexp  11815  prmfac1  11819  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  tgcl  12222  nninfalllemn  13191  nninfsellemdc  13195