Theorem expd 451

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

Hypothesis

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

Assertion

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

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	com12 32	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 449	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
4	3	com3r 85	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 383

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  expdimp  452  expcomd  453  expdcom  454  pm3.3  459  syland  497  exp32  629  exp4b  630  exp4c  634  exp4d  635  exp42  637  exp44  639  exp5c  642  exp5j  643  exp5l  644  impl  648  mpan2d  706  a2and  849  3impib  1254  exp5o  1278  ax7  1930  ralrimivv  2953  mob2  3353  reuind  3378  reupick3  3871  elpwunsn  4171  disjiun  4573  sotr2  4988  wefrc  5032  relop  5194  predpoirr  5625  predfrirr  5626  suctrOLD  5726  fnun  5911  mpteqb  6207  funopsn  6319  tpres  6371  fconst5  6376  funfvima  6396  dfwe2  6873  limuni3  6944  tfisi  6950  ordom  6966  funcnvuni  7012  f1oweALT  7043  frxp  7174  poxp  7176  wfr3g  7300  wfrlem12  7313  onfununi  7325  tz7.48lem  7423  oecl  7504  oaordex  7525  oaass  7528  omwordri  7539  odi  7546  omass  7547  omeu  7552  oen0  7553  oewordi  7558  oewordri  7559  nnarcl  7583  nnmass  7591  dif1en  8078  findcard2  8085  unblem1  8097  unblem2  8098  domunfican  8118  marypha1lem  8222  supiso  8264  inf3lem3  8410  epfrs  8490  karden  8641  infxpenlem  8719  iunfictbso  8820  dfac5  8834  dfac2  8836  kmlem1  8855  kmlem9  8863  infpssrlem3  9010  fin23lem25  9029  fin23lem30  9047  domtriomlem  9147  axdc3lem4  9158  axcclem  9162  zorn2lem7  9207  konigthlem  9269  wunr1om  9420  tskr1om  9468  gruen  9513  grur1a  9520  indpi  9608  genpnmax  9708  prlem934  9734  ltaddpr  9735  ltexprlem7  9743  ltaprlem  9745  axrrecex  9863  axpre-sup  9869  lelttr  10007  dedekind  10079  addid2  10098  nn0lt2  11317  fzind  11351  fnn0ind  11352  btwnz  11355  uzwo  11627  lbzbi  11652  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  ledivge1le  11777  xrlelttr  11863  qbtwnre  11904  xrsupsslem  12009  xrinfmsslem  12010  supxrun  12018  elfz0ubfz0  12312  elfzo0z  12377  fzofzim  12382  elfznelfzo  12439  fleqceilz  12515  fsequb  12636  leexp2r  12780  bernneq  12852  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdnd2  13285  swrdswrdlem  13311  swrdswrd  13312  wrd2ind  13329  swrdccatin1  13334  swrdccatin2  13338  swrdccatin12lem3  13341  repswswrd  13382  cshweqrep  13418  swrd2lsw  13543  2swrd2eqwrdeq  13544  wrdl3s3  13553  s3iunsndisj  13555  cau3lem  13942  climuni  14131  mulcn2  14174  dvdsabseq  14873  divalglem8  14961  ndvdssub  14971  rplpwr  15114  algcvgblem  15128  lcmf  15184  lcmftp  15187  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfdvdsb  15194  lcmfun  15196  cncongr1  15219  euclemma  15263  prmlem1a  15651  iscatd  16157  initoeu1  16484  initoeu2  16489  termoeu1  16491  plelttr  16795  grpinveu  17279  symgfixelsi  17678  efgred  17984  telgsumfzs  18209  srgmulgass  18354  srgbinom  18368  lspdisjb  18947  mplcoe5lem  19288  cply1mul  19485  coe1fzgsumd  19493  gsummoncoe1  19495  evl1gsumd  19542  cpmatacl  20340  cpmatmcllem  20342  basis2  20566  0ntr  20685  uncmp  21016  1stcrest  21066  txcls  21217  txcnp  21233  tx1stc  21263  fgss2  21488  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  metcnp3  22155  tngngp3  22270  reconn  22439  iscau4  22885  ellimc3  23449  ulmbdd  23956  ulmcn  23957  sinq12ge0  24064  logblog  24330  gausslemma2dlem3  24893  ax5seglem5  25613  ax5seg  25618  wlkiswwlk2lem3  26221  wlkiswwlk2  26225  wlklniswwlkn2  26228  usg2wlkeq  26236  wwlknred  26251  wwlknext  26252  wwlkextfun  26257  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem0  26316  wwlksubclwwlk  26332  erclwwlksym  26342  erclwwlknsym  26354  eleclclwwlkn  26360  cusgraisrusgra  26465  rusgranumwlk  26484  eupai  26494  frgrancvvdeqlemB  26565  frgrawopreglem5  26575  frg2woteq  26587  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  frgrareggt1  26643  frgrareg  26644  grpoinveu  26757  ococss  27536  shmodsi  27632  h1datomi  27824  hoaddsub  28059  adjmul  28335  chjatom  28600  atomli  28625  atcvat4i  28640  mdsymlem3  28648  mdsymlem5  28650  mdsymlem6  28651  sumdmdlem  28661  cdj3lem2a  28679  cdj3lem3a  28682  bnj1204  30334  cvmsdisj  30506  fundmpss  30910  dfon2lem6  30937  dfon2lem8  30939  frr3g  31023  frrlem11  31036  ifscgr  31321  lineext  31353  fscgr  31357  idinside  31361  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn3  31380  brsegle  31385  seglecgr12  31388  hilbert1.2  31432  exp5d  31466  exp5k  31468  nn0prpwlem  31487  bj-restb  32228  poimirlem26  32605  poimirlem29  32608  poimirlem32  32611  areacirc  32675  heibor1lem  32778  pridl  33006  pridlc  33040  dmnnzd  33044  prtlem11  33169  prtlem17  33179  ax12indn  33246  atcvrj0  33732  cvrat4  33747  athgt  33760  lplnexllnN  33868  2llnjN  33871  lvolnle3at  33886  lncmp  34087  paddclN  34146  pexmidlem4N  34277  cdleme17d3  34802  cdleme50trn2  34857  cdlemf2  34868  cdlemf  34869  cdlemj3  35129  cdlemk26b-3  35211  dihord5b  35566  isnacs3  36291  jm2.26  36587  sbiota1  37657  exbir  37705  tratrb  37767  onfrALT  37785  in2an  37854  pwtrrVD  38082  suctrALT2VD  38093  suctrALT2  38094  tratrbVD  38119  trintALTVD  38138  trintALT  38139  iccpartiltu  39960  iccpartigtl  39961  iccpartgt  39965  iccpartnel  39976  fmtnofac2lem  40018  fmtnofac2  40019  lighneallem2  40061  stgoldbwt  40198  bgoldbst  40200  sgoldbaltlem1  40201  riotaeqimp  40338  zm1nn  40348  2ffzoeq  40361  uhgrnbgr0nb  40576  cplgrop  40659  1wlkl1loop  40842  uspgr2wlkeq  40854  1wlkres  40879  upgrwlkdvdelem  40942  uhgr1wlkspthlem2  40960  pthdlem2lem  40973  isclWlkb  40980  crctisclwlk  41000  uspgrn2crct  41011  1wlkiswwlks2lem3  41068  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  wwlksnext  41099  wwlksnextfun  41104  rusgrnumwwlk  41178  clwlkclwwlklem2a4  41206  clwlkclwwlklem3  41210  erclwwlkssym  41242  erclwwlksnsym  41254  eleclclwwlksn  41260  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  conngrv2edg  41362  eupth2lem3lem6  41401  frgrncvvdeqlemB  41477  frgrwopreglem5  41485  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-frgrareggt1  41547  av-frgrareg  41548  lidldomn1  41711  ply1mulgsumlem1  41968  lincsumcl  42014  ellcoellss  42018  islinindfis  42032  lindslinindsimp1  42040  lindslinindsimp2lem5  42045  lindsrng01  42051  elfzolborelfzop1  42103  aacllem  42356