Theorem expd 416

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 415	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  expcomd  417  exp32  421  exp4b  431  exp4c  433  exp4d  434  exp42  436  exp44  438  exp5c  445  exp5j  446  exp5l  447  pm3.3  449  expdimp  453  impl  456  syland  603  mpan2d  691  a2and  842  3impib  1115  exp5o  1354  ralrimivv  3123  mob2  3651  reuind  3689  reupick3  4254  elpwunsn  4620  disjiun  5062  sotr2  5536  wefrc  5584  relop  5762  predpoirr  6240  predfrirr  6241  fnun  6554  mpteqb  6903  tpres  7085  fconst5  7090  funfvima  7115  riotaeqimp  7268  dfwe2  7633  limuni3  7708  tfisi  7714  trom  7730  funcnvuni  7787  f1oweALT  7824  frxp  7976  poxp  7978  wfr3g  8147  wfrlem12OLD  8160  onfununi  8181  tz7.48lem  8281  oecl  8376  oaordex  8398  oaass  8401  omwordri  8412  odi  8419  omass  8420  omeu  8425  oen0  8426  oewordi  8431  oewordri  8432  nnarcl  8456  nnmass  8464  findcard2  8956  dif1enALT  9059  findcard2OLD  9065  unblem1  9075  unblem2  9076  domunfican  9096  marypha1lem  9201  supiso  9243  inf3lem3  9397  epfrs  9498  frr3g  9523  karden  9662  infxpenlem  9778  iunfictbso  9879  dfac5  9893  dfac2b  9895  kmlem1  9915  kmlem9  9923  infpssrlem3  10070  fin23lem25  10089  fin23lem30  10107  domtriomlem  10207  axdc3lem4  10218  axcclem  10222  zorn2lem7  10267  konigthlem  10333  wunr1om  10484  tskr1om  10532  gruen  10577  grur1a  10584  indpi  10672  genpnmax  10772  prlem934  10798  ltaddpr  10799  ltexprlem7  10807  ltaprlem  10809  axrrecex  10928  axpre-sup  10934  lelttr  11074  dedekind  11147  addid2  11167  nn0lt2  12392  fzind  12427  fnn0ind  12428  btwnz  12432  uzwo  12660  lbzbi  12685  rpnnen1lem5  12730  ledivge1le  12810  xrlelttr  12899  qbtwnre  12942  xrsupsslem  13050  xrinfmsslem  13051  supxrun  13059  elfz1b  13334  elfz0ubfz0  13369  elfzo0z  13438  fzofzim  13443  elfznelfzo  13501  fleqceilz  13583  fsequb  13704  leexp2r  13901  bernneq  13953  fi1uzind  14220  brfi1indALT  14223  swrdnd0  14379  swrdswrdlem  14426  swrdswrd  14427  wrd2ind  14445  swrdccatin1  14447  swrdccatin2  14451  pfxccatin12lem3  14454  repswswrd  14506  cshweqrep  14543  swrd2lsw  14674  2swrd2eqwrdeq  14675  wrdl3s3  14686  s3iunsndisj  14688  cau3lem  15075  climuni  15270  mulcn2  15314  dvdsabseq  16031  divalglem8  16118  ndvdssub  16127  rplpwr  16276  algcvgblem  16291  lcmf  16347  lcmftp  16350  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfdvdsb  16357  lcmfun  16359  euclemma  16427  prmlem1a  16817  setsstruct2  16884  iscatd  17391  initoeu1  17735  initoeu2  17740  termoeu1  17742  plelttr  18071  insubm  18466  grpinveu  18623  cyccom  18831  symgfixelsi  19052  efgred  19363  telgsumfzs  19599  srgmulgass  19776  srgbinom  19790  lspdisjb  20397  mplcoe5lem  21249  cply1mul  21474  coe1fzgsumd  21482  gsummoncoe1  21484  evl1gsumd  21532  cpmatacl  21874  cpmatmcllem  21876  basis2  22110  0ntr  22231  uncmp  22563  1stcrest  22613  txcls  22764  txcnp  22780  tx1stc  22810  fgss2  23034  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  metcnp3  23705  tngngp3  23829  reconn  24000  iscau4  24452  ellimc3  25052  ulmbdd  25566  ulmcn  25567  sinq12ge0  25674  gausslemma2dlem3  26525  2sq2  26590  2sqreultlem  26604  2sqreunnltlem  26607  ax5seglem5  27310  ax5seg  27315  uhgrnbgr0nb  27730  cplgrop  27813  wlkl1loop  28014  uspgr2wlkeq  28022  upgrwlkdvdelem  28113  uhgrwkspthlem2  28131  pthdlem2lem  28144  uspgrn2crct  28182  wlkiswwlks2lem3  28245  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wwlksnext  28267  wwlksnextfun  28272  rusgrnumwwlk  28349  clwlkclwwlklem2a4  28370  clwlkclwwlklem3  28374  erclwwlksym  28394  erclwwlknsym  28443  eleclclwwlkn  28449  clwwlknonwwlknonb  28479  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  conngrv2edg  28568  eupth2lem3lem6  28606  frgrncvvdeqlem8  28679  frgrwopreglem4a  28683  frgrreggt1  28766  frgrreg  28767  grpoinveu  28890  ococss  29664  shmodsi  29760  h1datomi  29952  hoaddsub  30187  adjmul  30463  chjatom  30728  atomli  30753  atcvat4i  30768  mdsymlem3  30776  mdsymlem5  30778  mdsymlem6  30779  sumdmdlem  30789  cdj3lem2a  30807  cdj3lem3a  30810  bnj1204  33001  umgr2cycllem  33111  umgr2cycl  33112  cvmsdisj  33241  satfv0fun  33342  satffunlem  33372  satffunlem1lem2  33374  satffunlem2lem2  33377  fundmpss  33749  dfon2lem6  33773  dfon2lem8  33775  poxp2  33799  poxp3  33805  ssltleft  34063  ssltright  34064  ifscgr  34355  lineext  34387  fscgr  34391  idinside  34395  btwnconn1lem11  34408  btwnconn1lem12  34409  btwnconn3  34414  brsegle  34419  seglecgr12  34422  hilbert1.2  34466  exp5d  34500  exp5k  34502  nn0prpwlem  34520  bj-restb  35274  exrecfnlem  35559  poimirlem26  35812  poimirlem29  35815  poimirlem32  35818  areacirc  35879  heibor1lem  35976  pridl  36204  pridlc  36238  dmnnzd  36242  prtlem11  36887  prtlem17  36897  ax12indn  36964  atcvrj0  37449  cvrat4  37464  athgt  37477  lplnexllnN  37585  2llnjN  37588  lvolnle3at  37603  lncmp  37804  paddclN  37863  pexmidlem4N  37994  cdleme17d3  38517  cdleme50trn2  38572  cdlemf2  38583  cdlemf  38584  cdlemj3  38844  cdlemk26b-3  38926  dihord5b  39280  isnacs3  40539  jm2.26  40831  sbiota1  42059  exbir  42105  tratrb  42163  onfrALT  42176  in2an  42235  pwtrrVD  42452  suctrALT2VD  42463  suctrALT2  42464  tratrbVD  42488  trintALTVD  42507  trintALT  42508  or2expropbi  44539  fcoresf1  44574  2reu8i  44616  2reuimp  44618  zm1nn  44805  2ffzoeq  44831  iccpartiltu  44885  iccpartigtl  44886  iccpartgt  44890  iccpartnel  44901  sbcpr  44984  fmtnofac2lem  45031  fmtnofac2  45032  lighneallem2  45069  odd2prm2  45181  stgoldbwt  45239  sbgoldbst  45241  sbgoldbaltlem1  45242  mogoldbb  45248  isomuspgrlem1  45290  isomuspgrlem2d  45294  lidldomn1  45490  ply1mulgsumlem1  45738  lincsumcl  45783  ellcoellss  45787  islinindfis  45801  lindslinindsimp1  45809  lindslinindsimp2lem5  45814  lindsrng01  45820  elfzolborelfzop1  45871  rrx2linest  46099  aacllem  46516