Theorem 3exp 1125

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3expb  1126  3expib  1128  3com12  1129  3com13  1130  pm3.2an3  1347  3exp1  1359  3expd  1360  exp5o  1362  3ecase  1482  rexlimdv3a  3144  rabssdv  4005  reupick2  4259  disjiund  5063  otiunsndisj  5461  wefrc  5612  tz7.7  6336  unizlim  6434  funimassd  6893  fvelimad  6894  fveqdmss  7019  fompt  7059  f1oiso2  7296  ssorduni  7722  tfisi  7799  resf1extb  7874  funeldmdif  7990  poxp  8068  poseq  8098  fpr3g  8225  frrlem10  8235  smo11  8294  tfrlem5  8309  odi  8504  omass  8505  nndi  8549  nnmass  8550  naddoa  8628  undifixp  8872  findcard  9088  php3  9133  ac6sfi  9184  domunfican  9222  mapfien2  9312  fisup2g  9372  fiinf2g  9405  ttrclss  9632  ttrclselem2  9638  indcardi  9954  acndom  9964  ackbij1lem16  10147  infpssrlem4  10219  fin23lem11  10230  isfin2-2  10232  fin23lem34  10259  fin1a2lem10  10322  hsmexlem2  10340  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axcclem  10370  ttukeyg  10430  axdclem2  10433  axacndlem4  10524  axacndlem5  10525  axacnd  10526  tskr1om2  10682  tskwe2  10687  tskord  10694  tskcard  10695  tskuni  10697  tskwun  10698  gruiin  10724  grudomon  10731  gruina  10732  mulcanpi  10814  adderpq  10870  mulerpq  10871  dedekindle  11301  divgt0  12015  divge0  12016  nnne0  12202  nnadddir  12224  nnmulcom  12226  uzind  12612  uzind2  12613  iccsplit  13429  ssnn0fi  13938  expmordi  14120  sqlecan  14162  modexp  14191  expnngt1  14194  facavg  14254  2cshwcshw  14778  relexpcnv  14988  relexpaddnn  15004  relexpaddg  15006  pwdif  15824  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  fprodabs  15930  bpolycl  16008  bpolydif  16011  fprodefsum  16051  dvdsmodexp  16220  dvdsaddre2b  16267  nn0rppwr  16521  dvdsnprmd  16650  2mulprm  16653  prmndvdsfaclt  16686  ncoprmlnprm  16689  fermltl  16745  pceu  16808  setsstruct2  17135  setsstruct  17137  mreexexd  17605  isglbd  18466  symgpssefmnd  19362  pmtrfrn  19424  psgnunilem4  19463  ablsimpgprmd  20083  mulgass2  20281  islss4  20952  lspsneu  21116  lspfixed  21121  lspexch  21122  lsmcv  21134  lspsolvlem  21135  rnglidlmcl  21209  xrsdsreclblem  21388  nzerooringczr  21455  isphld  21629  mdetralt  22591  mdetunilem9  22603  fiinopn  22884  neips  23096  tpnei  23104  neindisj2  23106  opnneiid  23109  hausnei2  23336  cmpsublem  23382  cmpsub  23383  cmpcld  23385  comppfsc  23515  filufint  23903  cfinufil  23911  rnelfm  23936  alexsubALTlem1  24030  alexsubALTlem4  24033  alexsubALT  24034  tsmsxp  24138  neibl  24484  tngngp3  24639  tgqioo  24783  ovolunlem2  25483  iunmbl2  25542  itg1le  25698  vieta1  26296  aannenlem2  26313  aalioulem3  26318  aalioulem4  26319  aaliou2  26324  wilthlem3  27051  bcmono  27258  gausslemma2dlem1a  27346  sltstr  27797  sltsun1  27798  sltsun2  27799  ltslpss  27918  precsexlem8  28224  precsexlem9  28225  precsex  28228  onsfi  28366  oldfib  28387  expscllem  28440  expsgt0  28447  pw2cut  28470  pw2cut2  28472  bdaypw2n0bnd  28474  bdayfin  28497  iscgrglt  28600  axcontlem7  29057  elntg2  29072  edglnl  29230  numedglnl  29231  ausgrumgri  29254  ausgrusgri  29255  usgrausgrb  29256  usgredg2vtxeuALT  29309  ushgredgedg  29316  ushgredgedgloop  29318  nbuhgr2vtx1edgb  29439  cusgrsize2inds  29540  upgrewlkle2  29693  wlkl1loop  29724  redwlk  29757  pthdivtx  29813  pthdadjvtx  29814  upgr2pthnlp  29818  upgrspthswlk  29824  clwlkl1loop  29869  cyclnumvtx  29886  wwlksnred  29978  wwlksnextbi  29980  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  clwwlknwwlksn  30126  clwwlkinwwlk  30128  wwlksext2clwwlk  30145  1pthon2v  30241  uhgr3cyclex  30270  n4cyclfrgr  30379  frgrwopreg  30411  numclwwlk1lem2f1  30445  clwwlknonclwlknonf1o  30450  wlkl0  30455  frgrreggt1  30481  frgrreg  30482  frgrregord013  30483  chintcli  31420  spansnss  31660  elspansn4  31662  chscllem4  31729  hoadddir  31893  adjmul  32181  kbass6  32210  spansncv2  32382  sumdmdii  32504  nexple  32936  bnj1417  35223  lfuhgr2  35347  cusgredgex  35350  sat1el2xp  35607  fmlasuc  35614  satffunlem1lem1  35630  satffunlem2lem1  35632  mclsind  35798  iprodefisumlem  35968  btwndiff  36255  elicc3  36545  finminlem  36546  axtcond  36706  ttcmin  36724  sdclem2  38109  clmgmOLD  38218  grpomndo  38242  zerdivemp1x  38314  lsmsat  39500  lsmcv2  39521  lcvat  39522  lsatcveq0  39524  lcvexchlem4  39529  lcvexchlem5  39530  islshpcv  39545  l1cvpat  39546  lshpkrlem6  39607  omlfh3N  39751  cvlsupr4  39837  cvlsupr5  39838  cvlsupr6  39839  2llnneN  39901  hlrelat3  39904  cvrval3  39905  cvrval4N  39906  cvrexchlem  39911  2atlt  39931  cvrat4  39935  atbtwnexOLDN  39939  atbtwnex  39940  athgt  39948  3dim1  39959  3dim2  39960  3dim3  39961  1cvratex  39965  llnle  40010  atcvrlln2  40011  atcvrlln  40012  2llnmat  40016  lplnle  40032  lplnnle2at  40033  lplnnlelln  40035  llncvrlpln2  40049  2llnjN  40059  lvoli2  40073  lvolnlelln  40076  lvolnlelpln  40077  4atlem10  40098  4atlem11  40101  4atlem12  40104  lplncvrlvol2  40107  2lplnj  40112  lneq2at  40270  lnatexN  40271  lnjatN  40272  lncvrat  40274  2lnat  40276  cdlemb  40286  paddasslem14  40325  llnexchb2  40361  dalawlem10  40372  dalawlem13  40375  dalawlem14  40376  dalaw  40378  pclclN  40383  pclfinN  40392  osumcllem11N  40458  lhp2lt  40493  lhpexle3lem  40503  4atexlem7  40567  ldilcnv  40607  ldilco  40608  ltrncnv  40638  trlval2  40655  cdleme24  40844  cdleme26ee  40852  cdleme28  40865  cdleme32le  40939  cdleme50trn2  41043  cdleme50ltrn  41049  cdleme  41052  cdlemf1  41053  cdlemf  41055  cdlemg1cex  41080  cdlemg2ce  41084  cdlemg18b  41171  ltrnco  41211  tendocan  41316  cdlemk28-3  41400  cdlemk11t  41438  dia2dimlem6  41561  dia2dimlem12  41567  dihlsscpre  41726  dihord4  41750  dihord5b  41751  dihmeetlem3N  41797  dihmeetlem20N  41818  dvh4dimlem  41935  lclkrlem2y  42023  mapdpglem24  42196  mapdpglem32  42197  mapdpg  42198  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  mapdh9a  42281  mapdh9aOLDN  42282  hdmap14lem6  42365  hdmapglem7  42421  indstrd  42678  sn-addlid  42881  remulcand  42916  mzpexpmpt  43194  pellexlem5  43278  pellex  43280  pell14qrexpclnn0  43311  pellfundex  43331  monotuz  43386  monotoddzzfi  43387  rmxypos  43392  jm2.17a  43405  jm2.17b  43406  rmygeid  43409  jm2.19lem3  43436  jm2.15nn0  43448  jm2.16nn0  43449  aomclem2  43500  aomclem6  43504  dfac11  43507  hbtlem5  43573  cnsrexpcl  43610  cantnf2  43770  dflim5  43774  relexpxpnnidm  44147  relexpiidm  44148  relexpss1d  44149  iunrelexpmin1  44152  relexpmulnn  44153  iunrelexpmin2  44156  relexp01min  44157  relexp0a  44160  relexpxpmin  44161  relexpaddss  44162  trclimalb2  44170  tfindsd  44654  3impexpbicomi  44925  ee333  44951  eel12131  45156  eel2122old  45161  e333  45176  ordelordALTVD  45310  refsumcn  45478  uzwo4  45501  ssinc  45534  ssdec  45535  iunincfi  45541  restuni3  45565  eliuniin2  45567  rabssd  45589  reximdd  45595  suprnmpt  45621  disjf1o  45638  disjinfi  45639  ssnnf1octb  45641  choicefi  45646  mapssbi  45658  unirnmapsn  45659  iunmapsn  45662  rnmptlb  45687  rnmptbddlem  45688  infnsuprnmpt  45694  fperiodmullem  45751  upbdrech  45753  ssfiunibd  45757  supxrgere  45778  iuneqfzuzlem  45779  supxrgelem  45782  supxrge  45783  suplesup  45784  infrpge  45796  infleinf  45816  suplesup2  45820  supxrunb3  45843  infleinf2  45857  rexabslelem  45861  infrnmptle  45866  infxrunb3rnmpt  45871  iccshift  45963  iooshift  45967  fmul01  46025  fmuldfeq  46028  fmul01lt1  46031  mullimc  46061  islptre  46064  mullimcf  46068  limcperiod  46073  islpcn  46082  limsupre  46084  limcleqr  46087  neglimc  46090  addlimc  46091  0ellimcdiv  46092  limclner  46094  fnlimfvre  46117  limsuppnflem  46153  limsupmnfuzlem  46169  limsupre3lem  46175  limsupre3uzlem  46178  climuzlem  46186  limsupgtlem  46220  coskpi2  46309  cosknegpi  46312  cncfshift  46317  cncfperiod  46322  icccncfext  46330  dvnmptdivc  46381  dvnmptconst  46384  dvnmul  46386  dvmptfprodlem  46387  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  iblspltprt  46416  itgspltprt  46422  itgperiod  46424  ismbl3  46429  stoweidlem3  46446  stoweidlem31  46474  stoweidlem59  46502  stirlinglem13  46529  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem51  46600  fourierdlem70  46619  fourierdlem71  46620  fourierdlem73  46622  fourierdlem80  46629  fourierdlem81  46630  fourierdlem89  46638  fourierdlem91  46640  fourierdlem93  46642  fourierdlem97  46646  elaa2  46677  qndenserrnopnlem  46740  salexct  46777  subsaliuncl  46801  subsalsal  46802  sge0tsms  46823  sge0f1o  46825  sge0fsum  46830  sge0supre  46832  sge0sup  46834  sge0rnbnd  46836  sge0gerp  46838  sge0pnffigt  46839  sge0lefi  46841  sge0ltfirp  46843  sge0resrn  46847  sge0resplit  46849  sge0split  46852  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0rpcpnf  46864  sge0isum  46870  sge0xp  46872  sge0xaddlem2  46877  sge0uzfsumgt  46887  sge0seq  46889  sge0reuz  46890  nnfoctbdjlem  46898  nnfoctbdj  46899  iundjiun  46903  meadjiunlem  46908  voliunsge0lem  46915  meaiuninclem  46923  meaiininc2  46931  carageniuncllem1  46964  carageniuncllem2  46965  caratheodorylem1  46969  caratheodorylem2  46970  isomenndlem  46973  ovnsupge0  47000  ovnlerp  47005  ovncvrrp  47007  ovnsubaddlem1  47013  hoidmvval0  47030  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem2  47045  opnvonmbllem2  47076  ovnovollem3  47101  vonioo  47125  vonicc  47128  pimiooltgt  47153  sssmf  47181  smfaddlem1  47206  smflimlem6  47219  smfmullem4  47237  smfpimbor1lem1  47241  smfco  47245  smfpimcc  47251  smflimmpt  47253  smfinflem  47260  smflimsuplem7  47269  smflimsuplem8  47270  smflimsupmpt  47272  smfliminfmpt  47275  cfsetsnfsetf1  47522  nnmul2b  47794  2tceilhalfelfzo1  47799  elsetpreimafveqfv  47867  iccpartiltu  47897  sprsymrelfvlem  47965  reuopreuprim  48001  nprmmul2  48003  goldbachth  48025  fmtnofac1  48048  prmdvdsfmtnof1lem1  48062  lighneal  48089  grimuhgr  48378  uhgrimedgi  48381  uhgrimisgrgriclem  48421  clnbgrgrim  48425  grimedg  48426  usgrgrtrirex  48441  isubgr3stgrlem3  48459  isubgr3stgrlem6  48462  uspgrlimlem2  48480  grlimgrtri  48494  grlicsym  48504  clnbgr3stgrgrlic  48511  gpgusgralem  48547  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  uspgropssxp  48635  rngccatidALTV  48763  ringccatidALTV  48797  lcosslsp  48929  fllog2  49059  dignn0flhalf  49109  fv1arycl  49128  1arymaptf1  49133  fv2arycl  49139  2arymaptf1  49144  itschlc0yqe  49251  itsclc0xyqsol  49259  seposep  49416  iscnrm3lem6  49428  iunord  50166  setrec2fun  50182