Theorem 3exp 1132

Description: Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

Ref	Expression
3exp	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expa 1131	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 423	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1098

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  df-3an 1100

This theorem is referenced by:  3expb  1133  3expib  1135  3com12  1136  3com13  1137  pm3.2an3  1354  3exp1  1366  3expd  1367  exp5o  1369  3ecase  1495  rexlimdv3a  3167  rabssdv  4027  reupick2  4283  disjiund  5091  otiunsndisj  5489  wefrc  5641  tz7.7  6372  unizlim  6470  funimassd  6933  fvelimad  6934  fveqdmss  7059  fompt  7099  f1oiso2  7336  ssorduni  7762  tfisi  7839  resf1extb  7915  funeldmdif  8029  poxp  8108  poseq  8138  fpr3g  8266  frrlem10  8276  smo11  8335  tfrlem5  8350  odi  8548  omass  8549  nndi  8593  nnmass  8594  naddoa  8673  undifixp  8916  findcard  9132  php3  9177  ac6sfi  9228  domunfican  9266  mapfien2  9355  fisup2g  9415  fiinf2g  9448  ttrclss  9675  ttrclselem2  9681  indcardi  9997  acndom  10007  ackbij1lem16  10190  infpssrlem4  10263  fin23lem11  10274  isfin2-2  10276  fin23lem34  10303  fin1a2lem10  10366  hsmexlem2  10384  axcc3  10395  domtriomlem  10399  axdc3lem2  10408  axdc3lem4  10410  axcclem  10414  ttukeyg  10474  axdclem2  10477  axacndlem4  10568  axacndlem5  10569  axacnd  10570  tskr1om2  10726  tskwe2  10731  tskord  10738  tskcard  10739  tskuni  10741  tskwun  10742  gruiin  10768  grudomon  10775  gruina  10776  mulcanpi  10858  adderpq  10914  mulerpq  10915  dedekindle  11347  divgt0  12060  divge0  12061  nnne0  12247  nnadddir  12269  nnmulcom  12271  uzind  12665  uzind2  12666  iccsplit  13489  ssnn0fi  13998  expmordi  14180  sqlecan  14222  modexp  14251  expnngt1  14254  facavg  14314  2cshwcshw  14838  relexpcnv  15048  relexpaddnn  15064  relexpaddg  15066  pwdif  15898  prodfn0  15924  prodfrec  15925  ntrivcvgfvn0  15929  fprodabs  16004  bpolycl  16082  bpolydif  16085  fprodefsum  16125  dvdsmodexp  16294  dvdsaddre2b  16341  nn0rppwr  16595  dvdsnprmd  16724  2mulprm  16727  prmndvdsfaclt  16760  ncoprmlnprm  16763  fermltl  16819  pceu  16882  setsstruct2  17210  setsstruct  17212  mreexexd  17680  isglbd  18541  symgpssefmnd  19436  pmtrfrn  19498  psgnunilem4  19537  ablsimpgprmd  20157  mulgass2  20355  islss4  21026  lspsneu  21190  lspfixed  21195  lspexch  21196  lsmcv  21208  lspsolvlem  21209  rnglidlmcl  21283  xrsdsreclblem  21462  nzerooringczr  21529  isphld  21703  mdetralt  22665  mdetunilem9  22677  fiinopn  22958  neips  23170  tpnei  23178  neindisj2  23180  opnneiid  23183  hausnei2  23410  cmpsublem  23456  cmpsub  23457  cmpcld  23459  comppfsc  23589  filufint  23977  cfinufil  23985  rnelfm  24010  alexsubALTlem1  24104  alexsubALTlem4  24107  alexsubALT  24108  tsmsxp  24212  neibl  24558  tngngp3  24713  tgqioo  24857  ovolunlem2  25557  iunmbl2  25616  itg1le  25772  vieta1  26373  aannenlem2  26390  aalioulem3  26395  aalioulem4  26396  aaliou2  26401  wilthlem3  27131  bcmono  27338  gausslemma2dlem1a  27426  sltstr  27877  sltsun1  27878  sltsun2  27879  ltslpss  27998  precsexlem8  28304  precsexlem9  28305  precsex  28308  onsfi  28446  oldfib  28467  expscllem  28520  expsgt0  28527  pw2cut  28550  pw2cut2  28552  bdaypw2n0bnd  28554  bdayfin  28577  iscgrglt  28680  axcontlem7  29168  elntg2  29183  edglnl  29341  numedglnl  29342  ausgrumgri  29365  ausgrusgri  29366  usgrausgrb  29367  usgredg2vtxeuALT  29420  ushgredgedg  29427  ushgredgedgloop  29429  nbuhgr2vtx1edgb  29550  cusgrsize2inds  29651  upgrewlkle2  29804  wlkl1loop  29835  redwlk  29868  pthdivtx  29924  pthdadjvtx  29925  upgr2pthnlp  29929  upgrspthswlk  29935  clwlkl1loop  29980  cyclnumvtx  29997  wwlksnred  30089  wwlksnextbi  30091  elwwlks2ons3im  30151  usgrwwlks2on  30155  umgrwwlks2on  30156  clwwlknwwlksn  30237  clwwlkinwwlk  30239  wwlksext2clwwlk  30256  1pthon2v  30352  uhgr3cyclex  30381  n4cyclfrgr  30490  frgrwopreg  30522  numclwwlk1lem2f1  30556  clwwlknonclwlknonf1o  30561  wlkl0  30566  frgrreggt1  30592  frgrreg  30593  frgrregord013  30594  chintcli  31531  spansnss  31771  elspansn4  31773  chscllem4  31840  hoadddir  32004  adjmul  32292  kbass6  32321  spansncv2  32493  sumdmdii  32615  nexple  33032  bnj1417  35333  lfuhgr2  35466  cusgredgex  35469  sat1el2xp  35726  fmlasuc  35733  satffunlem1lem1  35749  satffunlem2lem1  35751  mclsind  35917  iprodefisumlem  36087  btwndiff  36374  elicc3  36674  finminlem  36675  axtcond  36835  ttcmin  36853  sdclem2  38238  clmgmOLD  38347  grpomndo  38371  zerdivemp1x  38443  lsmsat  39629  lsmcv2  39650  lcvat  39651  lsatcveq0  39653  lcvexchlem4  39658  lcvexchlem5  39659  islshpcv  39674  l1cvpat  39675  lshpkrlem6  39736  omlfh3N  39880  cvlsupr4  39966  cvlsupr5  39967  cvlsupr6  39968  2llnneN  40030  hlrelat3  40033  cvrval3  40034  cvrval4N  40035  cvrexchlem  40040  2atlt  40060  cvrat4  40064  atbtwnexOLDN  40068  atbtwnex  40069  athgt  40077  3dim1  40088  3dim2  40089  3dim3  40090  1cvratex  40094  llnle  40139  atcvrlln2  40140  atcvrlln  40141  2llnmat  40145  lplnle  40161  lplnnle2at  40162  lplnnlelln  40164  llncvrlpln2  40178  2llnjN  40188  lvoli2  40202  lvolnlelln  40205  lvolnlelpln  40206  4atlem10  40227  4atlem11  40230  4atlem12  40233  lplncvrlvol2  40236  2lplnj  40241  lneq2at  40399  lnatexN  40400  lnjatN  40401  lncvrat  40403  2lnat  40405  cdlemb  40415  paddasslem14  40454  llnexchb2  40490  dalawlem10  40501  dalawlem13  40504  dalawlem14  40505  dalaw  40507  pclclN  40512  pclfinN  40521  osumcllem11N  40587  lhp2lt  40622  lhpexle3lem  40632  4atexlem7  40696  ldilcnv  40736  ldilco  40737  ltrncnv  40767  trlval2  40784  cdleme24  40973  cdleme26ee  40981  cdleme28  40994  cdleme32le  41068  cdleme50trn2  41172  cdleme50ltrn  41178  cdleme  41181  cdlemf1  41182  cdlemf  41184  cdlemg1cex  41209  cdlemg2ce  41213  cdlemg18b  41300  ltrnco  41340  tendocan  41445  cdlemk28-3  41529  cdlemk11t  41567  dia2dimlem6  41690  dia2dimlem12  41696  dihlsscpre  41855  dihord4  41879  dihord5b  41880  dihmeetlem3N  41926  dihmeetlem20N  41947  dvh4dimlem  42064  lclkrlem2y  42152  mapdpglem24  42325  mapdpglem32  42326  mapdpg  42327  baerlem3lem2  42331  baerlem5alem2  42332  baerlem5blem2  42333  mapdh9a  42410  mapdh9aOLDN  42411  hdmap14lem6  42494  hdmapglem7  42550  indstrd  42807  sn-addlid  43010  remulcand  43045  mzpexpmpt  43323  pellexlem5  43407  pellex  43409  pell14qrexpclnn0  43440  pellfundex  43460  monotuz  43515  monotoddzzfi  43516  rmxypos  43521  jm2.17a  43534  jm2.17b  43535  rmygeid  43538  jm2.19lem3  43565  jm2.15nn0  43577  jm2.16nn0  43578  aomclem2  43629  aomclem6  43633  dfac11  43636  hbtlem5  43702  cnsrexpcl  43739  cantnf2  43899  dflim5  43903  relexpxpnnidm  44276  relexpiidm  44277  relexpss1d  44278  iunrelexpmin1  44281  relexpmulnn  44282  iunrelexpmin2  44285  relexp01min  44286  relexp0a  44289  relexpxpmin  44290  relexpaddss  44291  trclimalb2  44299  tfindsd  44783  3impexpbicomi  45054  ee333  45080  eel12131  45285  eel2122old  45290  e333  45305  ordelordALTVD  45439  refsumcn  45607  uzwo4  45630  ssinc  45662  ssdec  45663  iunincfi  45669  restuni3  45693  eliuniin2  45695  rabssd  45717  reximdd  45723  suprnmpt  45749  disjf1o  45766  disjinfi  45767  ssnnf1octb  45769  choicefi  45774  mapssbi  45786  unirnmapsn  45787  iunmapsn  45790  rnmptlb  45815  rnmptbddlem  45816  infnsuprnmpt  45822  fperiodmullem  45879  upbdrech  45881  ssfiunibd  45885  supxrgere  45906  iuneqfzuzlem  45907  supxrgelem  45910  supxrge  45911  suplesup  45912  infrpge  45924  infleinf  45944  suplesup2  45948  supxrunb3  45971  infleinf2  45985  rexabslelem  45989  infrnmptle  45994  infxrunb3rnmpt  45999  iccshift  46091  iooshift  46095  fmul01  46153  fmuldfeq  46156  fmul01lt1  46159  mullimc  46189  islptre  46192  mullimcf  46196  limcperiod  46201  islpcn  46210  limsupre  46212  limcleqr  46215  neglimc  46218  addlimc  46219  0ellimcdiv  46220  limclner  46222  fnlimfvre  46245  limsuppnflem  46281  limsupmnfuzlem  46297  limsupre3lem  46303  limsupre3uzlem  46306  climuzlem  46314  limsupgtlem  46348  coskpi2  46437  cosknegpi  46440  cncfshift  46445  cncfperiod  46450  icccncfext  46458  dvnmptdivc  46509  dvnmptconst  46512  dvnmul  46514  dvmptfprodlem  46515  dvmptfprod  46516  dvnprodlem1  46517  dvnprodlem2  46518  iblspltprt  46544  itgspltprt  46550  itgperiod  46552  ismbl3  46557  stoweidlem3  46574  stoweidlem31  46602  stoweidlem59  46630  stirlinglem13  46657  fourierdlem41  46719  fourierdlem42  46720  fourierdlem48  46725  fourierdlem51  46728  fourierdlem70  46747  fourierdlem71  46748  fourierdlem73  46750  fourierdlem80  46757  fourierdlem81  46758  fourierdlem89  46766  fourierdlem91  46768  fourierdlem93  46770  fourierdlem97  46774  elaa2  46805  qndenserrnopnlem  46868  salexct  46905  subsaliuncl  46929  subsalsal  46930  sge0tsms  46951  sge0f1o  46953  sge0fsum  46958  sge0supre  46960  sge0sup  46962  sge0rnbnd  46964  sge0gerp  46966  sge0pnffigt  46967  sge0lefi  46969  sge0ltfirp  46971  sge0resrn  46975  sge0resplit  46977  sge0split  46980  sge0iunmptlemfi  46984  sge0iunmptlemre  46986  sge0iunmpt  46989  sge0rpcpnf  46992  sge0isum  46998  sge0xp  47000  sge0xaddlem2  47005  sge0uzfsumgt  47015  sge0seq  47017  sge0reuz  47018  nnfoctbdjlem  47026  nnfoctbdj  47027  iundjiun  47031  meadjiunlem  47036  voliunsge0lem  47043  meaiuninclem  47051  meaiininc2  47059  carageniuncllem1  47092  carageniuncllem2  47093  caratheodorylem1  47097  caratheodorylem2  47098  isomenndlem  47101  ovnsupge0  47128  ovnlerp  47133  ovncvrrp  47135  ovnsubaddlem1  47141  hoidmvval0  47158  hoidmv1lelem3  47164  hoidmv1le  47165  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem3  47168  ovnhoilem2  47173  opnvonmbllem2  47204  ovnovollem3  47229  vonioo  47253  vonicc  47256  pimiooltgt  47281  smfaddlem1  47334  smflimlem6  47347  smfmullem4  47365  smfpimbor1lem1  47369  smfco  47373  smfpimcc  47379  smflimmpt  47381  smfinflem  47388  smflimsuplem7  47397  smflimsuplem8  47398  smflimsupmpt  47400  smfliminfmpt  47403  cfsetsnfsetf1  47650  nnmul2b  47922  2tceilhalfelfzo1  47927  elsetpreimafveqfv  47995  iccpartiltu  48025  sprsymrelfvlem  48093  reuopreuprim  48129  nprmmul2  48131  goldbachth  48153  fmtnofac1  48176  prmdvdsfmtnof1lem1  48190  lighneal  48217  grimuhgr  48506  uhgrimedgi  48509  uhgrimisgrgriclem  48549  clnbgrgrim  48553  grimedg  48554  usgrgrtrirex  48569  isubgr3stgrlem3  48587  isubgr3stgrlem6  48590  uspgrlimlem2  48608  grlimgrtri  48622  grlicsym  48632  clnbgr3stgrgrlic  48639  gpgusgralem  48675  gpgedgvtx1  48681  gpgvtxedg0  48682  gpgvtxedg1  48683  uspgropssxp  48763  rngccatidALTV  48891  ringccatidALTV  48925  lcosslsp  49057  fllog2  49187  dignn0flhalf  49237  fv1arycl  49256  1arymaptf1  49261  fv2arycl  49267  2arymaptf1  49272  itschlc0yqe  49379  itsclc0xyqsol  49387  seposep  49544  iscnrm3lem6  49556  iunord  50294  setrec2fun  50310