Theorem 3exp 1120

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3expb  1121  3expib  1123  3com12  1124  3com13  1125  pm3.2an3  1342  3exp1  1354  3expd  1355  exp5o  1357  3ecase  1477  rexlimdv3a  3142  rabssdv  4014  reupick2  4271  disjiund  5076  otiunsndisj  5474  wefrc  5625  tz7.7  6349  unizlim  6447  funimassd  6906  fvelimad  6907  fveqdmss  7030  fompt  7070  f1oiso2  7307  ssorduni  7733  tfisi  7810  resf1extb  7885  funeldmdif  8001  poxp  8078  poseq  8108  fpr3g  8235  frrlem10  8245  smo11  8304  tfrlem5  8319  odi  8514  omass  8515  nndi  8559  nnmass  8560  naddoa  8638  undifixp  8882  findcard  9098  php3  9143  ac6sfi  9194  domunfican  9232  mapfien2  9322  fisup2g  9382  fiinf2g  9415  ttrclss  9641  ttrclselem2  9647  indcardi  9963  acndom  9973  ackbij1lem16  10156  infpssrlem4  10228  fin23lem11  10239  isfin2-2  10241  fin23lem34  10268  fin1a2lem10  10331  hsmexlem2  10349  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axcclem  10379  ttukeyg  10439  axdclem2  10442  axacndlem4  10533  axacndlem5  10534  axacnd  10535  tskr1om2  10691  tskwe2  10696  tskord  10703  tskcard  10704  tskuni  10706  tskwun  10707  gruiin  10733  grudomon  10740  gruina  10741  mulcanpi  10823  adderpq  10879  mulerpq  10880  dedekindle  11310  divgt0  12024  divge0  12025  nnne0  12211  nnadddir  12233  nnmulcom  12235  uzind  12621  uzind2  12622  iccsplit  13438  ssnn0fi  13947  expmordi  14129  sqlecan  14171  modexp  14200  expnngt1  14203  facavg  14263  2cshwcshw  14787  relexpcnv  14997  relexpaddnn  15013  relexpaddg  15015  pwdif  15833  prodfn0  15859  prodfrec  15860  ntrivcvgfvn0  15864  fprodabs  15939  bpolycl  16017  bpolydif  16020  fprodefsum  16060  dvdsmodexp  16229  dvdsaddre2b  16276  nn0rppwr  16530  dvdsnprmd  16659  2mulprm  16662  prmndvdsfaclt  16695  ncoprmlnprm  16698  fermltl  16754  pceu  16817  setsstruct2  17144  setsstruct  17146  mreexexd  17614  isglbd  18475  symgpssefmnd  19371  pmtrfrn  19433  psgnunilem4  19472  ablsimpgprmd  20092  mulgass2  20290  islss4  20957  lspsneu  21121  lspfixed  21126  lspexch  21127  lsmcv  21139  lspsolvlem  21140  rnglidlmcl  21214  xrsdsreclblem  21393  nzerooringczr  21460  isphld  21634  mdetralt  22573  mdetunilem9  22585  fiinopn  22866  neips  23078  tpnei  23086  neindisj2  23088  opnneiid  23091  hausnei2  23318  cmpsublem  23364  cmpsub  23365  cmpcld  23367  comppfsc  23497  filufint  23885  cfinufil  23893  rnelfm  23918  alexsubALTlem1  24012  alexsubALTlem4  24015  alexsubALT  24016  tsmsxp  24120  neibl  24466  tngngp3  24621  tgqioo  24765  ovolunlem2  25465  iunmbl2  25524  itg1le  25680  vieta1  26278  aannenlem2  26295  aalioulem3  26300  aalioulem4  26301  aaliou2  26306  wilthlem3  27033  bcmono  27240  gausslemma2dlem1a  27328  sltstr  27779  sltsun1  27780  sltsun2  27781  ltslpss  27900  precsexlem8  28206  precsexlem9  28207  precsex  28210  onsfi  28348  oldfib  28369  expscllem  28422  expsgt0  28429  pw2cut  28452  pw2cut2  28454  bdaypw2n0bnd  28456  bdayfin  28479  iscgrglt  28582  axcontlem7  29039  elntg2  29054  edglnl  29212  numedglnl  29213  ausgrumgri  29236  ausgrusgri  29237  usgrausgrb  29238  usgredg2vtxeuALT  29291  ushgredgedg  29298  ushgredgedgloop  29300  nbuhgr2vtx1edgb  29421  cusgrsize2inds  29522  upgrewlkle2  29675  wlkl1loop  29706  redwlk  29739  pthdivtx  29795  pthdadjvtx  29796  upgr2pthnlp  29800  upgrspthswlk  29806  clwlkl1loop  29851  cyclnumvtx  29868  wwlksnred  29960  wwlksnextbi  29962  elwwlks2ons3im  30022  usgrwwlks2on  30026  umgrwwlks2on  30027  clwwlknwwlksn  30108  clwwlkinwwlk  30110  wwlksext2clwwlk  30127  1pthon2v  30223  uhgr3cyclex  30252  n4cyclfrgr  30361  frgrwopreg  30393  numclwwlk1lem2f1  30427  clwwlknonclwlknonf1o  30432  wlkl0  30437  frgrreggt1  30463  frgrreg  30464  frgrregord013  30465  chintcli  31402  spansnss  31642  elspansn4  31644  chscllem4  31711  hoadddir  31875  adjmul  32163  kbass6  32192  spansncv2  32364  sumdmdii  32486  nexple  32917  bnj1417  35183  lfuhgr2  35301  cusgredgex  35304  sat1el2xp  35561  fmlasuc  35568  satffunlem1lem1  35584  satffunlem2lem1  35586  mclsind  35752  iprodefisumlem  35922  btwndiff  36209  elicc3  36499  finminlem  36500  axtcond  36660  ttcmin  36678  sdclem2  38063  clmgmOLD  38172  grpomndo  38196  zerdivemp1x  38268  lsmsat  39454  lsmcv2  39475  lcvat  39476  lsatcveq0  39478  lcvexchlem4  39483  lcvexchlem5  39484  islshpcv  39499  l1cvpat  39500  lshpkrlem6  39561  omlfh3N  39705  cvlsupr4  39791  cvlsupr5  39792  cvlsupr6  39793  2llnneN  39855  hlrelat3  39858  cvrval3  39859  cvrval4N  39860  cvrexchlem  39865  2atlt  39885  cvrat4  39889  atbtwnexOLDN  39893  atbtwnex  39894  athgt  39902  3dim1  39913  3dim2  39914  3dim3  39915  1cvratex  39919  llnle  39964  atcvrlln2  39965  atcvrlln  39966  2llnmat  39970  lplnle  39986  lplnnle2at  39987  lplnnlelln  39989  llncvrlpln2  40003  2llnjN  40013  lvoli2  40027  lvolnlelln  40030  lvolnlelpln  40031  4atlem10  40052  4atlem11  40055  4atlem12  40058  lplncvrlvol2  40061  2lplnj  40066  lneq2at  40224  lnatexN  40225  lnjatN  40226  lncvrat  40228  2lnat  40230  cdlemb  40240  paddasslem14  40279  llnexchb2  40315  dalawlem10  40326  dalawlem13  40329  dalawlem14  40330  dalaw  40332  pclclN  40337  pclfinN  40346  osumcllem11N  40412  lhp2lt  40447  lhpexle3lem  40457  4atexlem7  40521  ldilcnv  40561  ldilco  40562  ltrncnv  40592  trlval2  40609  cdleme24  40798  cdleme26ee  40806  cdleme28  40819  cdleme32le  40893  cdleme50trn2  40997  cdleme50ltrn  41003  cdleme  41006  cdlemf1  41007  cdlemf  41009  cdlemg1cex  41034  cdlemg2ce  41038  cdlemg18b  41125  ltrnco  41165  tendocan  41270  cdlemk28-3  41354  cdlemk11t  41392  dia2dimlem6  41515  dia2dimlem12  41521  dihlsscpre  41680  dihord4  41704  dihord5b  41705  dihmeetlem3N  41751  dihmeetlem20N  41772  dvh4dimlem  41889  lclkrlem2y  41977  mapdpglem24  42150  mapdpglem32  42151  mapdpg  42152  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  mapdh9a  42235  mapdh9aOLDN  42236  hdmap14lem6  42319  hdmapglem7  42375  indstrd  42632  sn-addlid  42836  remulcand  42871  mzpexpmpt  43177  pellexlem5  43261  pellex  43263  pell14qrexpclnn0  43294  pellfundex  43314  monotuz  43369  monotoddzzfi  43370  rmxypos  43375  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.19lem3  43419  jm2.15nn0  43431  jm2.16nn0  43432  aomclem2  43483  aomclem6  43487  dfac11  43490  hbtlem5  43556  cnsrexpcl  43593  cantnf2  43753  dflim5  43757  relexpxpnnidm  44130  relexpiidm  44131  relexpss1d  44132  iunrelexpmin1  44135  relexpmulnn  44136  iunrelexpmin2  44139  relexp01min  44140  relexp0a  44143  relexpxpmin  44144  relexpaddss  44145  trclimalb2  44153  tfindsd  44637  3impexpbicomi  44908  ee333  44934  eel12131  45139  eel2122old  45144  e333  45159  ordelordALTVD  45293  refsumcn  45461  uzwo4  45484  ssinc  45517  ssdec  45518  iunincfi  45524  restuni3  45548  eliuniin2  45550  rabssd  45572  reximdd  45578  suprnmpt  45604  disjf1o  45621  disjinfi  45622  ssnnf1octb  45624  choicefi  45629  mapssbi  45642  unirnmapsn  45643  iunmapsn  45646  rnmptlb  45672  rnmptbddlem  45673  infnsuprnmpt  45679  fperiodmullem  45736  upbdrech  45738  ssfiunibd  45742  supxrgere  45763  iuneqfzuzlem  45764  supxrgelem  45767  supxrge  45768  suplesup  45769  infrpge  45781  infleinf  45801  suplesup2  45805  supxrunb3  45828  infleinf2  45842  rexabslelem  45846  infrnmptle  45851  infxrunb3rnmpt  45856  iccshift  45948  iooshift  45952  fmul01  46010  fmuldfeq  46013  fmul01lt1  46016  mullimc  46046  islptre  46049  mullimcf  46053  limcperiod  46058  islpcn  46067  limsupre  46069  limcleqr  46072  neglimc  46075  addlimc  46076  0ellimcdiv  46077  limclner  46079  fnlimfvre  46102  limsuppnflem  46138  limsupmnfuzlem  46154  limsupre3lem  46160  limsupre3uzlem  46163  climuzlem  46171  limsupgtlem  46205  coskpi2  46294  cosknegpi  46297  cncfshift  46302  cncfperiod  46307  icccncfext  46315  dvnmptdivc  46366  dvnmptconst  46369  dvnmul  46371  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  iblspltprt  46401  itgspltprt  46407  itgperiod  46409  ismbl3  46414  stoweidlem3  46431  stoweidlem31  46459  stoweidlem59  46487  stirlinglem13  46514  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem51  46585  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem80  46614  fourierdlem81  46615  fourierdlem89  46623  fourierdlem91  46625  fourierdlem93  46627  fourierdlem97  46631  elaa2  46662  qndenserrnopnlem  46725  salexct  46762  subsaliuncl  46786  subsalsal  46787  sge0tsms  46808  sge0f1o  46810  sge0fsum  46815  sge0supre  46817  sge0sup  46819  sge0rnbnd  46821  sge0gerp  46823  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resrn  46832  sge0resplit  46834  sge0split  46837  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0rpcpnf  46849  sge0isum  46855  sge0xp  46857  sge0xaddlem2  46862  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  nnfoctbdjlem  46883  nnfoctbdj  46884  iundjiun  46888  meadjiunlem  46893  voliunsge0lem  46900  meaiuninclem  46908  meaiininc2  46916  carageniuncllem1  46949  carageniuncllem2  46950  caratheodorylem1  46954  caratheodorylem2  46955  isomenndlem  46958  ovnsupge0  46985  ovnlerp  46990  ovncvrrp  46992  ovnsubaddlem1  46998  hoidmvval0  47015  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem2  47030  opnvonmbllem2  47061  ovnovollem3  47086  vonioo  47110  vonicc  47113  pimiooltgt  47138  sssmf  47166  smfaddlem1  47191  smflimlem6  47204  smfmullem4  47222  smfpimbor1lem1  47226  smfco  47230  smfpimcc  47236  smflimmpt  47238  smfinflem  47245  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  cfsetsnfsetf1  47507  nnmul2b  47779  2tceilhalfelfzo1  47784  elsetpreimafveqfv  47852  iccpartiltu  47882  sprsymrelfvlem  47950  reuopreuprim  47986  nprmmul2  47988  goldbachth  48010  fmtnofac1  48033  prmdvdsfmtnof1lem1  48047  lighneal  48074  grimuhgr  48363  uhgrimedgi  48366  uhgrimisgrgriclem  48406  clnbgrgrim  48410  grimedg  48411  usgrgrtrirex  48426  isubgr3stgrlem3  48444  isubgr3stgrlem6  48447  uspgrlimlem2  48465  grlimgrtri  48479  grlicsym  48489  clnbgr3stgrgrlic  48496  gpgusgralem  48532  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  uspgropssxp  48620  rngccatidALTV  48748  ringccatidALTV  48782  lcosslsp  48914  fllog2  49044  dignn0flhalf  49094  fv1arycl  49113  1arymaptf1  49118  fv2arycl  49124  2arymaptf1  49129  itschlc0yqe  49236  itsclc0xyqsol  49244  seposep  49401  iscnrm3lem6  49413  iunord  50151  setrec2fun  50167