Theorem expd 258

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)

Hypothesis

Ref	Expression
exp3a.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		exp3a.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	com12 30	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 115	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
4	3	com3r 79	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  expdimp  259  pm3.3  261  syland  293  exp32  365  exp4c  368  exp4d  369  exp42  371  exp44  373  exp5c  376  impl  380  mpan2d  432  a2and  564  pm2.6dc  874  3impib  1232  exp5o  1257  biassdc  1444  exbir  1486  expcomd  1491  expdcom  1492  mopick  2165  ralrimivv  2631  mob2  3006  reuind  3031  difin  3468  reupick3  3518  suctr  4566  tfisi  4734  relop  4930  funcnvuni  5450  fnun  5489  mpteqb  5796  funfvima  5950  riotaeqimp  6063  poxp  6468  nnmass  6760  rex2dom  7110  supisoti  7350  axprecex  8247  ltnsym  8411  nn0lt2  9729  fzind  9763  fnn0ind  9764  btwnz  9767  lbzbi  10018  ledivge1le  10129  elfz0ubfz0  10534  elfzo0z  10598  fzofzim  10602  flqeqceilz  10757  leexp2r  11032  bernneq  11100  swrdswrdlem  11478  swrdswrd  11479  wrd2ind  11497  swrdccatin1  11499  swrdccatin2  11503  pfxccatin12lem3  11506  cau3lem  11882  climuni  12061  mulcn2  12080  dvdsabseq  12616  ndvdssub  12699  bezoutlemmain  12777  rplpwr  12806  algcvgblem  12829  euclemma  12926  insubm  13794  grpinveu  13845  srgmulgass  14295  basis2  15151  txcnp  15374  metcnp3  15614  gausslemma2dlem3  16194  wlkl1loop  16611  wlk1walkdom  16612  uspgr2wlkeq  16618  eupth2lem3lem6fi  16724  lealltlt2  16764  bj-charfunr  16848