Theorem 3exp 1135

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 1134	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 424	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3expb  1136  3expib  1138  3com12  1139  3com13  1140  pm3.2an3  1357  3exp1  1369  3expd  1370  exp5o  1372  3ecase  1502  rexlimdv3a  3176  rabssdv  4036  reupick2  4292  disjiund  5104  otiunsndisj  5504  wefrc  5656  tz7.7  6387  unizlim  6486  funimassd  6948  fvelimad  6949  fveqdmss  7074  fompt  7114  f1oiso2  7351  ssorduni  7777  tfisi  7854  resf1extb  7930  funeldmdif  8044  poxp  8123  poseq  8153  fpr3g  8281  frrlem10  8291  smo11  8350  tfrlem5  8365  odi  8563  omass  8564  nndi  8608  nnmass  8609  naddoa  8688  undifixp  8931  findcard  9147  php3  9192  ac6sfi  9243  domunfican  9280  mapfien2  9368  fisup2g  9428  fiinf2g  9461  ttrclss  9688  ttrclselem2  9694  indcardi  10024  acndom  10034  ackbij1lem16  10216  infpssrlem4  10289  fin23lem11  10300  isfin2-2  10302  fin23lem34  10329  fin1a2lem10  10392  hsmexlem2  10410  axcc3  10421  domtriomlem  10425  axdc3lem2  10434  axdc3lem4  10436  axcclem  10440  ttukeyg  10500  axdclem2  10503  axacndlem4  10594  axacndlem5  10595  axacnd  10596  tskr1om2  10752  tskwe2  10757  tskord  10764  tskcard  10765  tskuni  10767  tskwun  10768  gruiin  10794  grudomon  10801  gruina  10802  mulcanpi  10884  adderpq  10940  mulerpq  10941  dedekindle  11373  divgt0  12082  divge0  12083  nnne0  12269  nnadddir  12291  nnmulcom  12293  uzind  12687  uzind2  12688  iccsplit  13511  ssnn0fi  14020  expmordi  14202  sqlecan  14244  modexp  14273  expnngt1  14276  facavg  14336  2cshwcshw  14861  relexpcnv  15071  relexpaddnn  15087  relexpaddg  15089  pwdif  15921  prodfn0  15947  prodfrec  15948  ntrivcvgfvn0  15952  fprodabs  16027  bpolycl  16105  bpolydif  16108  fprodefsum  16148  dvdsmodexp  16317  dvdsaddre2b  16364  nn0rppwr  16618  dvdsnprmd  16747  2mulprm  16750  prmndvdsfaclt  16783  ncoprmlnprm  16786  fermltl  16842  pceu  16905  setsstruct2  17233  setsstruct  17235  mreexexd  17703  isglbd  18564  symgpssefmnd  19465  pmtrfrn  19527  psgnunilem4  19566  ablsimpgprmd  20186  mulgass2  20391  islss4  21060  lspsneu  21224  lspfixed  21229  lspexch  21230  lsmcv  21242  lspsolvlem  21243  rnglidlmcl  21318  unichnlidl  21339  xrsdsreclblem  21531  nzerooringczr  21598  isphld  21772  mdetralt  22733  mdetunilem9  22745  fiinopn  23026  neips  23238  tpnei  23246  neindisj2  23248  opnneiid  23251  hausnei2  23478  cmpsublem  23524  cmpsub  23525  cmpcld  23527  comppfsc  23657  filufint  24045  cfinufil  24053  rnelfm  24078  alexsubALTlem1  24172  alexsubALTlem4  24175  alexsubALT  24176  tsmsxp  24280  neibl  24626  tngngp3  24781  tgqioo  24925  ovolunlem2  25625  iunmbl2  25684  itg1le  25840  vieta1  26441  aannenlem2  26458  aalioulem3  26463  aalioulem4  26464  aaliou2  26469  wilthlem3  27199  bcmono  27406  gausslemma2dlem1a  27494  sltstr  27945  sltsun1  27946  sltsun2  27947  ltslpss  28066  precsexlem8  28372  precsexlem9  28373  precsex  28376  onsfi  28514  oldfib  28535  expscllem  28588  expsgt0  28595  pw2cut  28618  pw2cut2  28620  bdaypw2n0bnd  28622  bdayfin  28645  iscgrglt  28748  axcontlem7  29260  elntg2  29275  edglnl  29433  numedglnl  29434  ausgrumgri  29457  ausgrusgri  29458  usgrausgrb  29459  usgredg2vtxeuALT  29512  ushgredgedg  29519  ushgredgedgloop  29521  nbuhgr2vtx1edgb  29642  cusgrsize2inds  29743  upgrewlkle2  29896  wlkl1loop  29927  redwlk  29960  pthdivtx  30016  pthdadjvtx  30017  upgr2pthnlp  30021  upgrspthswlk  30027  clwlkl1loop  30072  cyclnumvtx  30089  wwlksnred  30181  wwlksnextbi  30183  elwwlks2ons3im  30243  usgrwwlks2on  30247  umgrwwlks2on  30248  clwwlknwwlksn  30329  clwwlkinwwlk  30331  wwlksext2clwwlk  30348  1pthon2v  30444  uhgr3cyclex  30473  n4cyclfrgr  30582  frgrwopreg  30614  numclwwlk1lem2f1  30648  clwwlknonclwlknonf1o  30653  wlkl0  30658  frgrreggt1  30684  frgrreg  30685  frgrregord013  30686  chintcli  31623  spansnss  31863  elspansn4  31865  chscllem4  31932  hoadddir  32096  adjmul  32384  kbass6  32413  spansncv2  32585  sumdmdii  32707  nexple  33117  bnj1417  35373  lfuhgr2  35509  cusgredgex  35512  sat1el2xp  35769  fmlasuc  35776  satffunlem1lem1  35792  satffunlem2lem1  35794  mclsind  35960  iprodefisumlem  36130  btwndiff  36417  elicc3  36716  finminlem  36717  axtcond  36877  ttcmin  36895  sdclem2  38280  clmgmOLD  38389  grpomndo  38413  zerdivemp1x  38485  lsmsat  39671  lsmcv2  39692  lcvat  39693  lsatcveq0  39695  lcvexchlem4  39700  lcvexchlem5  39701  islshpcv  39716  l1cvpat  39717  lshpkrlem6  39778  omlfh3N  39922  cvlsupr4  40008  cvlsupr5  40009  cvlsupr6  40010  2llnneN  40072  hlrelat3  40075  cvrval3  40076  cvrval4N  40077  cvrexchlem  40082  2atlt  40102  cvrat4  40106  atbtwnexOLDN  40110  atbtwnex  40111  athgt  40119  3dim1  40130  3dim2  40131  3dim3  40132  1cvratex  40136  llnle  40181  atcvrlln2  40182  atcvrlln  40183  2llnmat  40187  lplnle  40203  lplnnle2at  40204  lplnnlelln  40206  llncvrlpln2  40220  2llnjN  40230  lvoli2  40244  lvolnlelln  40247  lvolnlelpln  40248  4atlem10  40269  4atlem11  40272  4atlem12  40275  lplncvrlvol2  40278  2lplnj  40283  lneq2at  40441  lnatexN  40442  lnjatN  40443  lncvrat  40445  2lnat  40447  cdlemb  40457  paddasslem14  40496  llnexchb2  40532  dalawlem10  40543  dalawlem13  40546  dalawlem14  40547  dalaw  40549  pclclN  40554  pclfinN  40563  osumcllem11N  40629  lhp2lt  40664  lhpexle3lem  40674  4atexlem7  40738  ldilcnv  40778  ldilco  40779  ltrncnv  40809  trlval2  40826  cdleme24  41015  cdleme26ee  41023  cdleme28  41036  cdleme32le  41110  cdleme50trn2  41214  cdleme50ltrn  41220  cdleme  41223  cdlemf1  41224  cdlemf  41226  cdlemg1cex  41251  cdlemg2ce  41255  cdlemg18b  41342  ltrnco  41382  tendocan  41487  cdlemk28-3  41571  cdlemk11t  41609  dia2dimlem6  41732  dia2dimlem12  41738  dihlsscpre  41897  dihord4  41921  dihord5b  41922  dihmeetlem3N  41968  dihmeetlem20N  41989  dvh4dimlem  42106  lclkrlem2y  42194  mapdpglem24  42367  mapdpglem32  42368  mapdpg  42369  baerlem3lem2  42373  baerlem5alem2  42374  baerlem5blem2  42375  mapdh9a  42452  mapdh9aOLDN  42453  hdmap14lem6  42536  hdmapglem7  42592  indstrd  42849  sn-addlid  43054  remulcand  43089  mzpexpmpt  43367  pellexlem5  43451  pellex  43453  pell14qrexpclnn0  43484  pellfundex  43504  monotuz  43559  monotoddzzfi  43560  rmxypos  43565  jm2.17a  43578  jm2.17b  43579  rmygeid  43582  jm2.19lem3  43609  jm2.15nn0  43621  jm2.16nn0  43622  aomclem2  43673  aomclem6  43677  dfac11  43680  hbtlem5  43746  cnsrexpcl  43783  cantnf2  43943  dflim5  43947  relexpxpnnidm  44320  relexpiidm  44321  relexpss1d  44322  iunrelexpmin1  44325  relexpmulnn  44326  iunrelexpmin2  44329  relexp01min  44330  relexp0a  44333  relexpxpmin  44334  relexpaddss  44335  trclimalb2  44343  tfindsd  44825  3impexpbicomi  45081  ee333  45107  eel12131  45312  eel2122old  45317  e333  45332  ordelordALTVD  45466  refsumcn  45641  uzwo4  45664  ssinc  45696  ssdec  45697  iunincfi  45703  restuni3  45727  eliuniin2  45729  rabssd  45751  reximdd  45757  suprnmpt  45783  disjf1o  45800  disjinfi  45801  ssnnf1octb  45803  choicefi  45808  mapssbi  45820  unirnmapsn  45821  iunmapsn  45824  rnmptlb  45849  rnmptbddlem  45850  infnsuprnmpt  45856  fperiodmullem  45913  upbdrech  45915  ssfiunibd  45919  supxrgere  45940  iuneqfzuzlem  45941  supxrgelem  45944  supxrge  45945  suplesup  45946  infrpge  45958  infleinf  45978  suplesup2  45982  supxrunb3  46005  infleinf2  46019  rexabslelem  46023  infrnmptle  46028  infxrunb3rnmpt  46033  iccshift  46125  iooshift  46129  fmul01  46187  fmuldfeq  46190  fmul01lt1  46193  mullimc  46223  islptre  46226  mullimcf  46230  limcperiod  46235  islpcn  46244  limsupre  46246  limcleqr  46249  neglimc  46252  addlimc  46253  0ellimcdiv  46254  limclner  46256  fnlimfvre  46279  limsuppnflem  46315  limsupmnfuzlem  46331  limsupre3lem  46337  limsupre3uzlem  46340  climuzlem  46348  limsupgtlem  46382  coskpi2  46471  cosknegpi  46474  cncfshift  46479  cncfperiod  46484  icccncfext  46492  dvnmptdivc  46543  dvnmptconst  46546  dvnmul  46548  dvmptfprodlem  46549  dvmptfprod  46550  dvnprodlem1  46551  dvnprodlem2  46552  iblspltprt  46578  itgspltprt  46584  itgperiod  46586  ismbl3  46591  stoweidlem3  46608  stoweidlem31  46636  stoweidlem59  46664  stirlinglem13  46691  fourierdlem41  46753  fourierdlem42  46754  fourierdlem48  46759  fourierdlem51  46762  fourierdlem70  46781  fourierdlem71  46782  fourierdlem73  46784  fourierdlem80  46791  fourierdlem81  46792  fourierdlem89  46800  fourierdlem91  46802  fourierdlem93  46804  fourierdlem97  46808  elaa2  46839  qndenserrnopnlem  46902  salexct  46939  subsaliuncl  46963  subsalsal  46964  sge0tsms  46985  sge0f1o  46987  sge0fsum  46992  sge0supre  46994  sge0sup  46996  sge0rnbnd  46998  sge0gerp  47000  sge0pnffigt  47001  sge0lefi  47003  sge0ltfirp  47005  sge0resrn  47009  sge0resplit  47011  sge0split  47014  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0iunmpt  47023  sge0rpcpnf  47026  sge0isum  47032  sge0xp  47034  sge0xaddlem2  47039  sge0uzfsumgt  47049  sge0seq  47051  sge0reuz  47052  nnfoctbdjlem  47060  nnfoctbdj  47061  iundjiun  47065  meadjiunlem  47070  voliunsge0lem  47077  meaiuninclem  47085  meaiininc2  47093  carageniuncllem1  47126  carageniuncllem2  47127  caratheodorylem1  47131  caratheodorylem2  47132  isomenndlem  47135  ovnsupge0  47162  ovnlerp  47167  ovncvrrp  47169  ovnsubaddlem1  47175  hoidmvval0  47192  hoidmv1lelem3  47198  hoidmv1le  47199  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem3  47202  ovnhoilem2  47207  opnvonmbllem2  47238  ovnovollem3  47263  vonioo  47287  vonicc  47290  pimiooltgt  47315  smfaddlem1  47368  smflimlem6  47381  smfmullem4  47399  smfpimbor1lem1  47403  smfco  47407  smfpimcc  47413  smflimmpt  47415  smfinflem  47422  smflimsuplem7  47431  smflimsuplem8  47432  smflimsupmpt  47434  smfliminfmpt  47437  cfsetsnfsetf1  47684  nnmul2b  47956  2tceilhalfelfzo1  47961  elsetpreimafveqfv  48029  iccpartiltu  48059  sprsymrelfvlem  48127  reuopreuprim  48163  nprmmul2  48165  goldbachth  48187  fmtnofac1  48210  prmdvdsfmtnof1lem1  48224  lighneal  48251  grimuhgr  48540  uhgrimedgi  48543  uhgrimisgrgriclem  48583  clnbgrgrim  48587  grimedg  48588  usgrgrtrirex  48603  isubgr3stgrlem3  48621  isubgr3stgrlem6  48624  uspgrlimlem2  48642  grlimgrtri  48656  grlicsym  48666  clnbgr3stgrgrlic  48673  gpgusgralem  48709  gpgedgvtx1  48715  gpgvtxedg0  48716  gpgvtxedg1  48717  uspgropssxp  48797  rngccatidALTV  48925  ringccatidALTV  48959  lcosslsp  49102  fllog2  49232  dignn0flhalf  49282  fv1arycl  49301  1arymaptf1  49306  fv2arycl  49312  2arymaptf1  49317  itschlc0yqe  49424  itsclc0xyqsol  49432  seposep  49588  iscnrm3lem6  49600  iunord  50338  setrec2fun  50354