Theorem 3exp 1137

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  3expb  1138  3expib  1140  3com12  1141  3com13  1142  pm3.2an3  1359  3exp1  1371  3expd  1372  exp5o  1374  3ecase  1505  rexlimdv3a  3170  rabssdv  4028  reupick2  4284  disjiund  5100  otiunsndisj  5503  wefrc  5655  tz7.7  6386  unizlim  6485  funimassd  6947  fvelimad  6948  fveqdmss  7073  fompt  7113  f1oiso2  7350  ssorduni  7774  tfisi  7851  resf1extb  7927  funeldmdif  8041  poxp  8120  poseq  8150  fpr3g  8278  frrlem10  8288  smo11  8347  tfrlem5  8362  odi  8560  omass  8561  nndi  8605  nnmass  8606  naddoa  8685  undifixp  8928  findcard  9144  php3  9189  ac6sfi  9240  domunfican  9277  mapfien2  9365  fisup2g  9425  fiinf2g  9458  ttrclss  9685  ttrclselem2  9691  indcardi  10021  acndom  10031  ackbij1lem16  10213  infpssrlem4  10285  fin23lem11  10296  isfin2-2  10298  fin23lem34  10325  fin1a2lem10  10388  hsmexlem2  10406  axcc3  10417  domtriomlem  10421  axdc3lem2  10430  axdc3lem4  10432  axcclem  10436  ttukeyg  10496  axdclem2  10499  axacndlem4  10590  axacndlem5  10591  axacnd  10592  tskr1om2  10748  tskwe2  10753  tskord  10760  tskcard  10761  tskuni  10763  tskwun  10764  gruiin  10790  grudomon  10797  gruina  10798  mulcanpi  10880  adderpq  10936  mulerpq  10937  dedekindle  11369  divgt0  12078  divge0  12079  nnne0  12265  nnadddir  12287  nnmulcom  12289  uzind  12683  uzind2  12684  iccsplit  13507  ssnn0fi  14017  expmordi  14199  sqlecan  14241  modexp  14270  expnngt1  14273  facavg  14333  2cshwcshw  14858  relexpcnv  15068  relexpaddnn  15084  relexpaddg  15086  pwdif  15918  prodfn0  15944  prodfrec  15945  ntrivcvgfvn0  15949  fprodabs  16024  bpolycl  16101  bpolydif  16104  fprodefsum  16144  dvdsmodexp  16313  dvdsaddre2b  16360  nn0rppwr  16614  dvdsnprmd  16743  2mulprm  16746  prmndvdsfaclt  16779  ncoprmlnprm  16782  fermltl  16838  pceu  16901  setsstruct2  17229  setsstruct  17231  mreexexd  17699  isglbd  18560  symgpssefmnd  19461  pmtrfrn  19523  psgnunilem4  19562  ablsimpgprmd  20182  mulgass2  20388  islss4  21083  lspsneu  21247  lspfixed  21252  lspexch  21253  lsmcv  21265  lspsolvlem  21266  rnglidlmcl  21341  unichnlidl  21362  xrsdsreclblem  21563  nzerooringczr  21630  isphld  21804  mdetralt  22765  mdetunilem9  22777  fiinopn  23058  neips  23270  tpnei  23278  neindisj2  23280  opnneiid  23283  hausnei2  23510  cmpsublem  23556  cmpsub  23557  cmpcld  23559  comppfsc  23689  filufint  24077  cfinufil  24085  rnelfm  24110  alexsubALTlem1  24204  alexsubALTlem4  24207  alexsubALT  24208  tsmsxp  24312  neibl  24658  tngngp3  24813  tgqioo  24957  ovolunlem2  25657  iunmbl2  25716  itg1le  25872  vieta1  26473  aannenlem2  26492  aalioulem3  26497  aalioulem4  26498  aaliou2  26503  wilthlem3  27234  bcmono  27441  gausslemma2dlem1a  27529  sltstr  27980  sltsun1  27981  sltsun2  27982  ltslpss  28101  precsexlem8  28407  precsexlem9  28408  precsex  28411  onsfi  28549  oldfib  28570  expscllem  28623  expsgt0  28630  pw2cut  28653  pw2cut2  28655  bdaypw2n0bnd  28657  bdayfin  28680  iscgrglt  28783  axcontlem7  29320  elntg2  29335  edglnl  29493  numedglnl  29494  ausgrumgri  29517  ausgrusgri  29518  usgrausgrb  29519  usgredg2vtxeuALT  29572  ushgredgedg  29579  ushgredgedgloop  29581  nbuhgr2vtx1edgb  29702  cusgrsize2inds  29803  upgrewlkle2  29956  wlkl1loop  29987  redwlk  30020  pthdivtx  30076  pthdadjvtx  30077  upgr2pthnlp  30081  upgrspthswlk  30087  clwlkl1loop  30132  cyclnumvtx  30149  wwlksnred  30241  wwlksnextbi  30243  elwwlks2ons3im  30303  usgrwwlks2on  30307  umgrwwlks2on  30308  clwwlknwwlksn  30389  clwwlkinwwlk  30391  wwlksext2clwwlk  30408  1pthon2v  30504  uhgr3cyclex  30533  n4cyclfrgr  30642  frgrwopreg  30674  numclwwlk1lem2f1  30708  clwwlknonclwlknonf1o  30713  wlkl0  30718  frgrreggt1  30744  frgrreg  30745  frgrregord013  30746  chintcli  31683  spansnss  31923  elspansn4  31925  chscllem4  31992  hoadddir  32156  adjmul  32444  kbass6  32473  spansncv2  32645  sumdmdii  32767  nexple  33177  bnj1417  35429  lfuhgr2  35611  cusgredgex  35614  sat1el2xp  35871  fmlasuc  35878  satffunlem1lem1  35894  satffunlem2lem1  35896  mclsind  36062  iprodefisumlem  36232  btwndiff  36519  elicc3  36828  finminlem  36829  axtcond  36989  ttcmin  37007  sdclem2  38393  clmgmOLD  38502  grpomndo  38526  zerdivemp1x  38598  lsmsat  39782  lsmcv2  39803  lcvat  39804  lsatcveq0  39806  lcvexchlem4  39811  lcvexchlem5  39812  islshpcv  39827  l1cvpat  39828  lshpkrlem6  39889  omlfh3N  40033  cvlsupr4  40119  cvlsupr5  40120  cvlsupr6  40121  2llnneN  40183  hlrelat3  40186  cvrval3  40187  cvrval4N  40188  cvrexchlem  40193  2atlt  40213  cvrat4  40217  atbtwnexOLDN  40221  atbtwnex  40222  athgt  40230  3dim1  40241  3dim2  40242  3dim3  40243  1cvratex  40247  llnle  40292  atcvrlln2  40293  atcvrlln  40294  2llnmat  40298  lplnle  40314  lplnnle2at  40315  lplnnlelln  40317  llncvrlpln2  40331  2llnjN  40341  lvoli2  40355  lvolnlelln  40358  lvolnlelpln  40359  4atlem10  40380  4atlem11  40383  4atlem12  40386  lplncvrlvol2  40389  2lplnj  40394  lneq2at  40552  lnatexN  40553  lnjatN  40554  lncvrat  40556  2lnat  40558  cdlemb  40568  paddasslem14  40607  llnexchb2  40643  dalawlem10  40654  dalawlem13  40657  dalawlem14  40658  dalaw  40660  pclclN  40665  pclfinN  40674  osumcllem11N  40740  lhp2lt  40775  lhpexle3lem  40785  4atexlem7  40849  ldilcnv  40889  ldilco  40890  ltrncnv  40920  trlval2  40937  cdleme24  41126  cdleme26ee  41134  cdleme28  41147  cdleme32le  41221  cdleme50trn2  41325  cdleme50ltrn  41331  cdleme  41334  cdlemf1  41335  cdlemf  41337  cdlemg1cex  41362  cdlemg2ce  41366  cdlemg18b  41453  ltrnco  41493  tendocan  41598  cdlemk28-3  41682  cdlemk11t  41720  dia2dimlem6  41843  dia2dimlem12  41849  dihlsscpre  42008  dihord4  42032  dihord5b  42033  dihmeetlem3N  42079  dihmeetlem20N  42100  dvh4dimlem  42217  lclkrlem2y  42305  mapdpglem24  42478  mapdpglem32  42479  mapdpg  42480  baerlem3lem2  42484  baerlem5alem2  42485  baerlem5blem2  42486  mapdh9a  42563  mapdh9aOLDN  42564  hdmap14lem6  42647  hdmapglem7  42703  indstrd  42960  sn-addlid  43165  remulcand  43200  mzpexpmpt  43476  pellexlem5  43560  pellex  43562  pell14qrexpclnn0  43593  pellfundex  43613  monotuz  43668  monotoddzzfi  43669  rmxypos  43674  jm2.17a  43687  jm2.17b  43688  rmygeid  43691  jm2.19lem3  43718  jm2.15nn0  43730  jm2.16nn0  43731  aomclem2  43782  aomclem6  43786  dfac11  43789  hbtlem5  43855  cnsrexpcl  43892  cantnf2  44052  dflim5  44056  relexpxpnnidm  44429  relexpiidm  44430  relexpss1d  44431  iunrelexpmin1  44434  relexpmulnn  44435  iunrelexpmin2  44438  relexp01min  44439  relexp0a  44442  relexpxpmin  44443  relexpaddss  44444  trclimalb2  44452  tfindsd  44934  3impexpbicomi  45190  ee333  45216  eel12131  45421  eel2122old  45426  e333  45441  ordelordALTVD  45575  refsumcn  45750  uzwo4  45773  ssinc  45805  ssdec  45806  iunincfi  45812  restuni3  45836  eliuniin2  45838  rabssd  45860  reximdd  45866  suprnmpt  45892  disjf1o  45909  disjinfi  45910  ssnnf1octb  45912  choicefi  45917  mapssbi  45929  unirnmapsn  45930  iunmapsn  45933  rnmptlb  45958  rnmptbddlem  45959  infnsuprnmpt  45965  fperiodmullem  46022  upbdrech  46024  ssfiunibd  46028  supxrgere  46049  iuneqfzuzlem  46050  supxrgelem  46053  supxrge  46054  suplesup  46055  infrpge  46067  infleinf  46087  suplesup2  46091  supxrunb3  46114  infleinf2  46128  rexabslelem  46132  infrnmptle  46137  infxrunb3rnmpt  46142  iccshift  46234  iooshift  46238  fmul01  46296  fmuldfeq  46299  fmul01lt1  46302  mullimc  46332  islptre  46335  mullimcf  46339  limcperiod  46344  islpcn  46353  limsupre  46355  limcleqr  46358  neglimc  46361  addlimc  46362  0ellimcdiv  46363  limclner  46365  fnlimfvre  46388  limsuppnflem  46424  limsupmnfuzlem  46440  limsupre3lem  46446  limsupre3uzlem  46449  climuzlem  46457  limsupgtlem  46491  coskpi2  46580  cosknegpi  46583  cncfshift  46588  cncfperiod  46593  icccncfext  46601  dvnmptdivc  46652  dvnmptconst  46655  dvnmul  46657  dvmptfprodlem  46658  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem2  46661  iblspltprt  46687  itgspltprt  46693  itgperiod  46695  ismbl3  46700  stoweidlem3  46717  stoweidlem31  46745  stoweidlem59  46773  stirlinglem13  46800  fourierdlem41  46862  fourierdlem42  46863  fourierdlem48  46868  fourierdlem51  46871  fourierdlem70  46890  fourierdlem71  46891  fourierdlem73  46893  fourierdlem80  46900  fourierdlem81  46901  fourierdlem89  46909  fourierdlem91  46911  fourierdlem93  46913  fourierdlem97  46917  elaa2  46948  qndenserrnopnlem  47011  salexct  47048  subsaliuncl  47072  subsalsal  47073  sge0tsms  47094  sge0f1o  47096  sge0fsum  47101  sge0supre  47103  sge0sup  47105  sge0rnbnd  47107  sge0gerp  47109  sge0pnffigt  47110  sge0lefi  47112  sge0ltfirp  47114  sge0resrn  47118  sge0resplit  47120  sge0split  47123  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0iunmpt  47132  sge0rpcpnf  47135  sge0isum  47141  sge0xp  47143  sge0xaddlem2  47148  sge0uzfsumgt  47158  sge0seq  47160  sge0reuz  47161  nnfoctbdjlem  47169  nnfoctbdj  47170  iundjiun  47174  meadjiunlem  47179  voliunsge0lem  47186  meaiuninclem  47194  meaiininc2  47202  carageniuncllem1  47235  carageniuncllem2  47236  caratheodorylem1  47240  caratheodorylem2  47241  isomenndlem  47244  ovnsupge0  47271  ovnlerp  47276  ovncvrrp  47278  ovnsubaddlem1  47284  hoidmvval0  47301  hoidmv1lelem3  47307  hoidmv1le  47308  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  ovnhoilem2  47316  opnvonmbllem2  47347  ovnovollem3  47372  vonioo  47396  vonicc  47399  pimiooltgt  47424  smfaddlem1  47477  smflimlem6  47490  smfmullem4  47508  smfpimbor1lem1  47512  smfco  47516  smfpimcc  47522  smflimmpt  47524  smfinflem  47531  smflimsuplem7  47540  smflimsuplem8  47541  smflimsupmpt  47543  smfliminfmpt  47546  cfsetsnfsetf1  47796  nnmul2b  48068  2tceilhalfelfzo1  48073  elsetpreimafveqfv  48141  iccpartiltu  48171  sprsymrelfvlem  48239  reuopreuprim  48275  nprmmul2  48277  goldbachth  48299  fmtnofac1  48322  prmdvdsfmtnof1lem1  48336  lighneal  48363  grimuhgr  48652  uhgrimedgi  48655  uhgrimisgrgriclem  48695  clnbgrgrim  48699  grimedg  48700  usgrgrtrirex  48715  isubgr3stgrlem3  48733  isubgr3stgrlem6  48736  uspgrlimlem2  48754  grlimgrtri  48768  grlicsym  48778  clnbgr3stgrgrlic  48785  gpgusgralem  48821  gpgedgvtx1  48827  gpgvtxedg0  48828  gpgvtxedg1  48829  uspgropssxp  48909  rngccatidALTV  49037  ringccatidALTV  49071  lcosslsp  49218  fllog2  49348  dignn0flhalf  49398  fv1arycl  49417  1arymaptf1  49422  fv2arycl  49428  2arymaptf1  49433  itschlc0yqe  49540  itsclc0xyqsol  49548  seposep  49704  iscnrm3lem6  49716  iunord  50454  setrec2fun  50470