Theorem expd 418

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expdcom 417	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  expcomd  419  exp32  423  exp4b  433  exp4c  435  exp4d  436  exp42  438  exp44  440  exp5c  447  exp5j  448  exp5l  449  pm3.3  451  expdimp  455  impl  458  syland  604  mpan2d  692  a2and  841  3impib  1112  exp5o  1351  ralrimivv  3190  mob2  3705  reuind  3743  reupick3  4287  elpwunsn  4614  disjiun  5045  sotr2  5499  wefrc  5543  relop  5715  predpoirr  6170  predfrirr  6171  fnun  6457  mpteqb  6781  tpres  6957  fconst5  6962  funfvima  6986  riotaeqimp  7134  dfwe2  7490  limuni3  7561  tfisi  7567  ordom  7583  funcnvuni  7630  f1oweALT  7667  frxp  7814  poxp  7816  wfr3g  7947  wfrlem12  7960  onfununi  7972  tz7.48lem  8071  oecl  8156  oaordex  8178  oaass  8181  omwordri  8192  odi  8199  omass  8200  omeu  8205  oen0  8206  oewordi  8211  oewordri  8212  nnarcl  8236  nnmass  8244  dif1en  8745  findcard2  8752  unblem1  8764  unblem2  8765  domunfican  8785  marypha1lem  8891  supiso  8933  inf3lem3  9087  epfrs  9167  karden  9318  infxpenlem  9433  iunfictbso  9534  dfac5  9548  dfac2b  9550  kmlem1  9570  kmlem9  9578  infpssrlem3  9721  fin23lem25  9740  fin23lem30  9758  domtriomlem  9858  axdc3lem4  9869  axcclem  9873  zorn2lem7  9918  konigthlem  9984  wunr1om  10135  tskr1om  10183  gruen  10228  grur1a  10235  indpi  10323  genpnmax  10423  prlem934  10449  ltaddpr  10450  ltexprlem7  10458  ltaprlem  10460  axrrecex  10579  axpre-sup  10585  lelttr  10725  dedekind  10797  addid2  10817  nn0lt2  12039  fzind  12074  fnn0ind  12075  btwnz  12078  uzwo  12305  lbzbi  12330  rpnnen1lem5  12374  ledivge1le  12454  xrlelttr  12543  qbtwnre  12586  xrsupsslem  12694  xrinfmsslem  12695  supxrun  12703  elfz1b  12970  elfz0ubfz0  13005  elfzo0z  13073  fzofzim  13078  elfznelfzo  13136  fleqceilz  13216  fsequb  13337  leexp2r  13532  bernneq  13584  fi1uzind  13849  brfi1indALT  13852  swrdnd0  14013  swrdswrdlem  14060  swrdswrd  14061  wrd2ind  14079  swrdccatin1  14081  swrdccatin2  14085  pfxccatin12lem3  14088  repswswrd  14140  cshweqrep  14177  swrd2lsw  14308  2swrd2eqwrdeq  14309  wrdl3s3  14320  s3iunsndisj  14322  cau3lem  14708  climuni  14903  mulcn2  14946  dvdsabseq  15657  divalglem8  15745  ndvdssub  15754  rplpwr  15901  algcvgblem  15915  lcmf  15971  lcmftp  15974  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  lcmfdvdsb  15981  lcmfun  15983  euclemma  16051  prmlem1a  16434  setsstruct2  16515  iscatd  16938  initoeu1  17265  initoeu2  17270  termoeu1  17272  plelttr  17576  insubm  17977  grpinveu  18132  cyccom  18340  symgfixelsi  18557  efgred  18868  telgsumfzs  19103  srgmulgass  19275  srgbinom  19289  lspdisjb  19892  mplcoe5lem  20242  cply1mul  20456  coe1fzgsumd  20464  gsummoncoe1  20466  evl1gsumd  20514  cpmatacl  21318  cpmatmcllem  21320  basis2  21553  0ntr  21673  uncmp  22005  1stcrest  22055  txcls  22206  txcnp  22222  tx1stc  22252  fgss2  22476  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALTlem4  22652  metcnp3  23144  tngngp3  23259  reconn  23430  iscau4  23876  ellimc3  24471  ulmbdd  24980  ulmcn  24981  sinq12ge0  25088  gausslemma2dlem3  25938  2sq2  26003  2sqreultlem  26017  2sqreunnltlem  26020  ax5seglem5  26713  ax5seg  26718  uhgrnbgr0nb  27130  cplgrop  27213  wlkl1loop  27413  uspgr2wlkeq  27421  upgrwlkdvdelem  27511  uhgrwkspthlem2  27529  pthdlem2lem  27542  uspgrn2crct  27580  wlkiswwlks2lem3  27643  wlkiswwlks2  27647  wlkiswwlksupgr2  27649  wlklnwwlkln2lem  27654  wwlksnext  27665  wwlksnextfun  27670  rusgrnumwwlk  27748  clwlkclwwlklem2a4  27769  clwlkclwwlklem3  27773  erclwwlksym  27793  erclwwlknsym  27843  eleclclwwlkn  27849  clwwlknonwwlknonb  27879  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  conngrv2edg  27968  eupth2lem3lem6  28006  frgrncvvdeqlem8  28079  frgrwopreglem4a  28083  frgrreggt1  28166  frgrreg  28167  grpoinveu  28290  ococss  29064  shmodsi  29160  h1datomi  29352  hoaddsub  29587  adjmul  29863  chjatom  30128  atomli  30153  atcvat4i  30168  mdsymlem3  30176  mdsymlem5  30178  mdsymlem6  30179  sumdmdlem  30189  cdj3lem2a  30207  cdj3lem3a  30210  bnj1204  32279  umgr2cycllem  32382  umgr2cycl  32383  cvmsdisj  32512  satfv0fun  32613  satffunlem  32643  satffunlem1lem2  32645  satffunlem2lem2  32648  fundmpss  33004  dfon2lem6  33028  dfon2lem8  33030  frr3g  33116  ifscgr  33500  lineext  33532  fscgr  33536  idinside  33540  btwnconn1lem11  33553  btwnconn1lem12  33554  btwnconn3  33559  brsegle  33564  seglecgr12  33567  hilbert1.2  33611  exp5d  33645  exp5k  33647  nn0prpwlem  33665  bj-restb  34379  exrecfnlem  34654  poimirlem26  34912  poimirlem29  34915  poimirlem32  34918  areacirc  34981  heibor1lem  35081  pridl  35309  pridlc  35343  dmnnzd  35347  prtlem11  35996  prtlem17  36006  ax12indn  36073  atcvrj0  36558  cvrat4  36573  athgt  36586  lplnexllnN  36694  2llnjN  36697  lvolnle3at  36712  lncmp  36913  paddclN  36972  pexmidlem4N  37103  cdleme17d3  37626  cdleme50trn2  37681  cdlemf2  37692  cdlemf  37693  cdlemj3  37953  cdlemk26b-3  38035  dihord5b  38389  isnacs3  39300  jm2.26  39592  sbiota1  40759  exbir  40805  tratrb  40863  onfrALT  40876  in2an  40935  pwtrrVD  41152  suctrALT2VD  41163  suctrALT2  41164  tratrbVD  41188  trintALTVD  41207  trintALT  41208  or2expropbi  43263  2reu8i  43306  2reuimp  43308  zm1nn  43496  2ffzoeq  43522  iccpartiltu  43576  iccpartigtl  43577  iccpartgt  43581  iccpartnel  43592  sbcpr  43677  fmtnofac2lem  43724  fmtnofac2  43725  lighneallem2  43765  odd2prm2  43877  stgoldbwt  43935  sbgoldbst  43937  sbgoldbaltlem1  43938  mogoldbb  43944  isomuspgrlem1  43986  isomuspgrlem2d  43990  lidldomn1  44186  ply1mulgsumlem1  44434  lincsumcl  44480  ellcoellss  44484  islinindfis  44498  lindslinindsimp1  44506  lindslinindsimp2lem5  44511  lindsrng01  44517  elfzolborelfzop1  44568  rrx2linest  44723  aacllem  44896