Theorem expd 419

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  expcomd  420  exp32  424  exp4b  434  exp4c  436  exp4d  437  exp42  439  exp44  441  exp5c  448  exp5j  449  exp5l  450  pm3.3  452  expdimp  456  impl  459  syland  612  mpan2d  704  a2and  856  3impib  1128  exp5o  1368  ralrimivv  3202  mob2  3677  reuind  3715  reupick3  4282  elpwunsn  4642  disjiun  5087  sotr2  5587  wefrc  5639  relop  5820  predpoirr  6316  predfrirr  6317  fnun  6631  mpteqb  6991  tpres  7181  fconst5  7186  funfvima  7210  riotaeqimp  7375  dfwe2  7753  limuni3  7828  tfisi  7835  trom  7851  funcnvuni  7909  resf1ext2b  7912  f1oweALT  7949  frxp  8101  poxp  8103  poxp2  8118  poxp3  8125  wfr3g  8295  onfununi  8307  tz7.48lem  8407  oecl  8501  oaordex  8522  oaass  8525  omwordri  8536  odi  8543  omass  8544  omeu  8549  oen0  8551  oewordi  8556  oewordri  8557  nnarcl  8581  nnmass  8589  brinxper  8703  findcard2  9129  rex2dom  9193  dif1ennnALT  9217  unblem1  9232  unblem2  9233  domunfican  9262  marypha1lem  9376  supiso  9419  inf3lem3  9582  epfrs  9683  frr3g  9711  karden  9850  infxpenlem  9966  iunfictbso  10067  dfac5  10082  dfac2b  10084  kmlem1  10104  kmlem9  10112  infpssrlem3  10259  fin23lem25  10278  fin23lem30  10296  domtriomlem  10396  axdc3lem4  10407  axcclem  10411  zorn2lem7  10456  konigthlem  10523  wunr1om  10674  tskr1om  10722  gruen  10767  grur1a  10774  indpi  10862  genpnmax  10962  prlem934  10988  ltaddpr  10989  ltexprlem7  10997  ltaprlem  10999  axrrecex  11118  axpre-sup  11124  lelttr  11270  dedekind  11343  addlid  11363  nn0lt2  12633  fzind  12668  fnn0ind  12669  btwnz  12673  uzwo  12909  lbzbi  12934  rpnnen1lem5  12979  ledivge1le  13063  xrlelttr  13155  qbtwnre  13199  xrsupsslem  13307  xrinfmsslem  13308  supxrun  13316  elfz1b  13595  elfz0ubfz0  13634  elfzo0z  13704  fzofzim  13712  elfznelfzo  13776  fleqceilz  13861  fsequb  13985  leexp2r  14184  bernneq  14239  fi1uzind  14517  brfi1indALT  14520  swrdnd0  14668  swrdswrdlem  14714  swrdswrd  14715  wrd2ind  14733  swrdccatin1  14735  swrdccatin2  14739  pfxccatin12lem3  14742  repswswrd  14794  cshweqrep  14831  swrd2lsw  14962  2swrd2eqwrdeq  14963  wrdl3s3  14972  s3iunsndisj  14978  cau3lem  15365  climuni  15562  mulcn2  15606  dvdsabseq  16330  divalglem8  16417  ndvdssub  16426  rplpwr  16575  algcvgblem  16594  lcmf  16650  lcmftp  16653  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfdvdsb  16660  lcmfun  16662  euclemma  16731  prmlem1a  17125  setsstruct2  17193  iscatd  17688  initoeu1  18027  initoeu2  18032  termoeu1  18034  plelttr  18357  insubm  18835  grpinveu  18999  cyccom  19227  symgfixelsi  19458  efgred  19771  telgsumfzs  20012  srgmulgass  20246  srgbinom  20260  lspdisjb  21176  mplcoe5lem  22072  cply1mul  22339  coe1fzgsumd  22347  gsummoncoe1  22351  evl1gsumd  22400  cpmatacl  22756  cpmatmcllem  22758  basis2  22991  0ntr  23111  uncmp  23443  1stcrest  23493  txcls  23644  txcnp  23660  tx1stc  23690  fgss2  23914  alexsubALTlem2  24088  alexsubALTlem3  24089  alexsubALTlem4  24090  metcnp3  24580  tngngp3  24696  reconn  24869  iscau4  25321  ellimc3  25921  ulmbdd  26438  ulmcn  26439  sinq12ge0  26550  gausslemma2dlem3  27409  2sq2  27474  2sqreultlem  27488  2sqreunnltlem  27491  sltsleft  27930  sltsright  27931  noseqind  28362  oldfib  28447  expsgt0  28507  bdayfinbndlem1  28537  bdayfin  28557  elreno2  28565  ax5seglem5  29080  ax5seg  29085  uhgrnbgr0nb  29501  cplgrop  29584  wlkl1loop  29784  uspgr2wlkeq  29792  upgrwlkdvdelem  29882  uhgrwkspthlem2  29900  pthdlem2lem  29913  uspgrn2crct  29954  wlkiswwlks2lem3  30017  wlkiswwlks2  30021  wlkiswwlksupgr2  30023  wlklnwwlkln2lem  30028  wwlksnext  30039  wwlksnextfun  30044  rusgrnumwwlk  30124  clwlkclwwlklem2a4  30145  clwlkclwwlklem3  30149  erclwwlksym  30169  erclwwlknsym  30218  eleclclwwlkn  30224  clwwlknonwwlknonb  30254  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  conngrv2edg  30343  eupth2lem3lem6  30381  frgrncvvdeqlem8  30454  frgrwopreglem4a  30458  frgrreggt1  30541  frgrreg  30542  grpoinveu  30668  ococss  31442  shmodsi  31538  h1datomi  31730  hoaddsub  31965  adjmul  32241  chjatom  32506  atomli  32531  atcvat4i  32546  mdsymlem3  32554  mdsymlem5  32556  mdsymlem6  32557  sumdmdlem  32567  cdj3lem2a  32585  cdj3lem3a  32588  bnj1204  35271  fineqvinfep  35385  umgr2cycllem  35454  umgr2cycl  35455  cvmsdisj  35584  satfv0fun  35685  satffunlem  35715  satffunlem1lem2  35717  satffunlem2lem2  35720  fundmpss  36081  dfon2lem6  36100  dfon2lem8  36102  ifscgr  36358  lineext  36390  fscgr  36394  idinside  36398  btwnconn1lem11  36411  btwnconn1lem12  36412  btwnconn3  36417  brsegle  36422  seglecgr12  36425  hilbert1.2  36469  exp5d  36626  exp5k  36628  nn0prpwlem  36646  mh-inf3f1  36865  bj-restb  37548  exrecfnlem  37837  poimirlem26  38109  poimirlem29  38112  poimirlem32  38115  areacirc  38176  heibor1lem  38272  pridl  38500  pridlc  38534  dmnnzd  38538  disjlem17  39365  membpartlem19  39377  prtlem11  39454  prtlem17  39464  ax12indn  39531  atcvrj0  40016  cvrat4  40031  athgt  40044  lplnexllnN  40152  2llnjN  40155  lvolnle3at  40170  lncmp  40371  paddclN  40430  pexmidlem4N  40561  cdleme17d3  41084  cdleme50trn2  41139  cdlemf2  41150  cdlemf  41151  cdlemj3  41411  cdlemk26b-3  41493  dihord5b  41847  isnacs3  43255  jm2.26  43543  ordnexbtwnsuc  43808  omabs2  43873  naddgeoa  43935  sbiota1  44974  exbir  45019  tratrb  45076  onfrALT  45089  in2an  45148  pwtrrVD  45364  suctrALT2VD  45375  suctrALT2  45376  tratrbVD  45400  trintALTVD  45419  trintALT  45420  or2expropbi  47592  fcoresf1  47627  2reu8i  47671  2reuimp  47673  zm1nn  47860  2ffzoeq  47886  iccpartiltu  47992  iccpartigtl  47993  iccpartgt  47997  iccpartnel  48008  sbcpr  48091  fmtnofac2lem  48141  fmtnofac2  48142  lighneallem2  48179  odd2prm2  48304  stgoldbwt  48362  sbgoldbst  48364  sbgoldbaltlem1  48365  mogoldbb  48371  uhgrimisgrgric  48517  clnbgrgrim  48520  grimedg  48521  gpgedgvtx1  48648  gpgedg2iv  48653  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem6  48710  pgnbgreunbgr  48711  lidldomn1  48817  ply1mulgsumlem1  48972  lincsumcl  49017  ellcoellss  49021  islinindfis  49035  lindslinindsimp1  49043  lindslinindsimp2lem5  49048  lindsrng01  49054  elfzolborelfzop1  49105  rrx2linest  49328  aacllem  50386