Theorem 3exp 1118

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3expb  1119  3expib  1121  3com12  1122  3com13  1123  pm3.2an3  1339  3exp1  1351  3expd  1352  exp5o  1354  3ecase  1473  rexlimdv3a  3156  rabssdv  4084  reupick2  4336  disjiund  5138  otiunsndisj  5529  wefrc  5682  tz7.7  6411  unizlim  6508  funimassd  6974  fvelimad  6975  fveqdmss  7097  fompt  7137  f1oiso2  7371  ssorduni  7797  sucexeloniOLD  7829  suceloniOLD  7831  tfisi  7879  funeldmdif  8071  poxp  8151  poseq  8181  fpr3g  8308  frrlem10  8318  smo11  8402  tfrlem5  8418  odi  8615  omass  8616  nndi  8659  nnmass  8660  naddoa  8738  undifixp  8972  findcard  9201  php3  9246  ac6sfi  9317  domunfican  9358  mapfien2  9446  fisup2g  9505  fiinf2g  9537  ttrclss  9757  ttrclselem2  9763  indcardi  10078  acndom  10088  ackbij1lem16  10271  infpssrlem4  10343  fin23lem11  10354  isfin2-2  10356  fin23lem34  10383  fin1a2lem10  10446  hsmexlem2  10464  axcc3  10475  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axcclem  10494  ttukeyg  10554  axdclem2  10557  axacndlem4  10647  axacndlem5  10648  axacnd  10649  tskr1om2  10805  tskwe2  10810  tskord  10817  tskcard  10818  tskuni  10820  tskwun  10821  gruiin  10847  grudomon  10854  gruina  10855  mulcanpi  10937  adderpq  10993  mulerpq  10994  dedekindle  11422  divgt0  12133  divge0  12134  nnne0  12297  uzind  12707  uzind2  12708  iccsplit  13521  ssnn0fi  14022  expmordi  14203  sqlecan  14244  modexp  14273  expnngt1  14276  facavg  14336  2cshwcshw  14860  relexpcnv  15070  relexpaddnn  15086  relexpaddg  15088  pwdif  15900  prodfn0  15926  prodfrec  15927  ntrivcvgfvn0  15931  fprodabs  16006  bpolycl  16084  bpolydif  16087  fprodefsum  16127  dvdsmodexp  16294  dvdsaddre2b  16340  nn0rppwr  16594  dvdsnprmd  16723  2mulprm  16726  prmndvdsfaclt  16758  ncoprmlnprm  16761  fermltl  16817  pceu  16879  setsstruct2  17207  setsstruct  17209  mreexexd  17692  isglbd  18566  symgpssefmnd  19427  pmtrfrn  19490  psgnunilem4  19529  ablsimpgprmd  20149  mulgass2  20322  islss4  20977  lspsneu  21142  lspfixed  21147  lspexch  21148  lsmcv  21160  lspsolvlem  21161  rnglidlmcl  21243  xrsdsreclblem  21447  nzerooringczr  21508  isphld  21689  mdetralt  22629  mdetunilem9  22641  fiinopn  22922  neips  23136  tpnei  23144  neindisj2  23146  opnneiid  23149  hausnei2  23376  cmpsublem  23422  cmpsub  23423  cmpcld  23425  comppfsc  23555  filufint  23943  cfinufil  23951  rnelfm  23976  alexsubALTlem1  24070  alexsubALTlem4  24073  alexsubALT  24074  tsmsxp  24178  neibl  24529  tngngp3  24692  tgqioo  24835  ovolunlem2  25546  iunmbl2  25605  itg1le  25762  vieta1  26368  aannenlem2  26385  aalioulem3  26390  aalioulem4  26391  aaliou2  26396  wilthlem3  27127  bcmono  27335  gausslemma2dlem1a  27423  sslttr  27866  ssltun1  27867  ssltun2  27868  sltlpss  27959  precsexlem8  28252  precsexlem9  28253  precsex  28256  expscl  28427  expsgt0  28429  pw2cut  28434  iscgrglt  28536  axcontlem7  28999  elntg2  29014  edglnl  29174  numedglnl  29175  ausgrumgri  29198  ausgrusgri  29199  usgrausgrb  29200  usgredg2vtxeuALT  29253  ushgredgedg  29260  ushgredgedgloop  29262  nbuhgr2vtx1edgb  29383  cusgrsize2inds  29485  upgrewlkle2  29638  wlkl1loop  29670  redwlk  29704  pthdivtx  29761  pthdadjvtx  29762  upgr2pthnlp  29764  upgrspthswlk  29770  clwlkl1loop  29815  wwlksnred  29921  wwlksnextbi  29923  elwwlks2ons3im  29983  umgrwwlks2on  29986  clwwlknwwlksn  30066  clwwlkinwwlk  30068  wwlksext2clwwlk  30085  1pthon2v  30181  uhgr3cyclex  30210  n4cyclfrgr  30319  frgrwopreg  30351  numclwwlk1lem2f1  30385  clwwlknonclwlknonf1o  30390  wlkl0  30395  frgrreggt1  30421  frgrreg  30422  frgrregord013  30423  chintcli  31359  spansnss  31599  elspansn4  31601  chscllem4  31668  hoadddir  31832  adjmul  32120  kbass6  32149  spansncv2  32321  sumdmdii  32443  nexple  33989  bnj1417  35033  lfuhgr2  35102  cusgredgex  35105  sat1el2xp  35363  fmlasuc  35370  satffunlem1lem1  35386  satffunlem2lem1  35388  mclsind  35554  iprodefisumlem  35719  btwndiff  36008  elicc3  36299  finminlem  36300  sdclem2  37728  clmgmOLD  37837  grpomndo  37861  zerdivemp1x  37933  lsmsat  38989  lsmcv2  39010  lcvat  39011  lsatcveq0  39013  lcvexchlem4  39018  lcvexchlem5  39019  islshpcv  39034  l1cvpat  39035  lshpkrlem6  39096  omlfh3N  39240  cvlsupr4  39326  cvlsupr5  39327  cvlsupr6  39328  2llnneN  39391  hlrelat3  39394  cvrval3  39395  cvrval4N  39396  cvrexchlem  39401  2atlt  39421  cvrat4  39425  atbtwnexOLDN  39429  atbtwnex  39430  athgt  39438  3dim1  39449  3dim2  39450  3dim3  39451  1cvratex  39455  llnle  39500  atcvrlln2  39501  atcvrlln  39502  2llnmat  39506  lplnle  39522  lplnnle2at  39523  lplnnlelln  39525  llncvrlpln2  39539  2llnjN  39549  lvoli2  39563  lvolnlelln  39566  lvolnlelpln  39567  4atlem10  39588  4atlem11  39591  4atlem12  39594  lplncvrlvol2  39597  2lplnj  39602  lneq2at  39760  lnatexN  39761  lnjatN  39762  lncvrat  39764  2lnat  39766  cdlemb  39776  paddasslem14  39815  llnexchb2  39851  dalawlem10  39862  dalawlem13  39865  dalawlem14  39866  dalaw  39868  pclclN  39873  pclfinN  39882  osumcllem11N  39948  lhp2lt  39983  lhpexle3lem  39993  4atexlem7  40057  ldilcnv  40097  ldilco  40098  ltrncnv  40128  trlval2  40145  cdleme24  40334  cdleme26ee  40342  cdleme28  40355  cdleme32le  40429  cdleme50trn2  40533  cdleme50ltrn  40539  cdleme  40542  cdlemf1  40543  cdlemf  40545  cdlemg1cex  40570  cdlemg2ce  40574  cdlemg18b  40661  ltrnco  40701  tendocan  40806  cdlemk28-3  40890  cdlemk11t  40928  dia2dimlem6  41051  dia2dimlem12  41057  dihlsscpre  41216  dihord4  41240  dihord5b  41241  dihmeetlem3N  41287  dihmeetlem20N  41308  dvh4dimlem  41425  lclkrlem2y  41513  mapdpglem24  41686  mapdpglem32  41687  mapdpg  41688  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  mapdh9a  41771  mapdh9aOLDN  41772  hdmap14lem6  41855  hdmapglem7  41911  indstrd  42174  nnadddir  42283  nnmulcom  42285  sn-addlid  42410  remulcand  42444  mzpexpmpt  42732  pellexlem5  42820  pellex  42822  pell14qrexpclnn0  42853  pellfundex  42873  monotuz  42929  monotoddzzfi  42930  rmxypos  42935  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  jm2.19lem3  42979  jm2.15nn0  42991  jm2.16nn0  42992  aomclem2  43043  aomclem6  43047  dfac11  43050  hbtlem5  43116  cnsrexpcl  43153  cantnf2  43314  dflim5  43318  relexpxpnnidm  43692  relexpiidm  43693  relexpss1d  43694  iunrelexpmin1  43697  relexpmulnn  43698  iunrelexpmin2  43701  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  relexpaddss  43707  trclimalb2  43715  tfindsd  44200  3impexpbicomi  44477  ee333  44504  eel12131  44710  eel2122old  44715  e333  44730  ordelordALTVD  44864  refsumcn  44967  uzwo4  44992  ssinc  45026  ssdec  45027  iunincfi  45033  restuni3  45057  eliuniin2  45059  rabssd  45081  reximdd  45090  suprnmpt  45116  disjf1o  45133  disjinfi  45134  ssnnf1octb  45136  choicefi  45142  mapssbi  45155  unirnmapsn  45156  iunmapsn  45159  rnmptlb  45187  rnmptbddlem  45188  infnsuprnmpt  45194  fperiodmullem  45253  upbdrech  45255  ssfiunibd  45259  supxrgere  45282  iuneqfzuzlem  45283  supxrgelem  45286  supxrge  45287  suplesup  45288  infrpge  45300  infleinf  45321  suplesup2  45325  supxrunb3  45348  infleinf2  45363  rexabslelem  45367  infrnmptle  45372  infxrunb3rnmpt  45377  iccshift  45470  iooshift  45474  fmul01  45535  fmuldfeq  45538  fmul01lt1  45541  mullimc  45571  islptre  45574  mullimcf  45578  limcperiod  45583  islpcn  45594  limsupre  45596  limcleqr  45599  neglimc  45602  addlimc  45603  0ellimcdiv  45604  limclner  45606  fnlimfvre  45629  limsuppnflem  45665  limsupmnfuzlem  45681  limsupre3lem  45687  limsupre3uzlem  45690  climuzlem  45698  limsupgtlem  45732  coskpi2  45821  cosknegpi  45824  cncfshift  45829  cncfperiod  45834  icccncfext  45842  dvnmptdivc  45893  dvnmptconst  45896  dvnmul  45898  dvmptfprodlem  45899  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem2  45902  iblspltprt  45928  itgspltprt  45934  itgperiod  45936  ismbl3  45941  stoweidlem3  45958  stoweidlem31  45986  stoweidlem59  46014  stirlinglem13  46041  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem51  46112  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem80  46141  fourierdlem81  46142  fourierdlem89  46150  fourierdlem91  46152  fourierdlem93  46154  fourierdlem97  46158  elaa2  46189  qndenserrnopnlem  46252  salexct  46289  subsaliuncl  46313  subsalsal  46314  sge0tsms  46335  sge0f1o  46337  sge0fsum  46342  sge0supre  46344  sge0sup  46346  sge0rnbnd  46348  sge0gerp  46350  sge0pnffigt  46351  sge0lefi  46353  sge0ltfirp  46355  sge0resrn  46359  sge0resplit  46361  sge0split  46364  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0rpcpnf  46376  sge0isum  46382  sge0xp  46384  sge0xaddlem2  46389  sge0uzfsumgt  46399  sge0seq  46401  sge0reuz  46402  nnfoctbdjlem  46410  nnfoctbdj  46411  iundjiun  46415  meadjiunlem  46420  voliunsge0lem  46427  meaiuninclem  46435  meaiininc2  46443  carageniuncllem1  46476  carageniuncllem2  46477  caratheodorylem1  46481  caratheodorylem2  46482  isomenndlem  46485  ovnsupge0  46512  ovnlerp  46517  ovncvrrp  46519  ovnsubaddlem1  46525  hoidmvval0  46542  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem2  46557  opnvonmbllem2  46588  ovnovollem3  46613  vonioo  46637  vonicc  46640  pimiooltgt  46665  sssmf  46693  smfaddlem1  46718  smflimlem6  46731  smfmullem4  46749  smfpimbor1lem1  46753  smfco  46757  smfpimcc  46763  smflimmpt  46765  smfinflem  46772  smflimsuplem7  46781  smflimsuplem8  46782  smflimsupmpt  46784  smfliminfmpt  46787  cfsetsnfsetf1  47008  elsetpreimafveqfv  47316  iccpartiltu  47346  sprsymrelfvlem  47414  reuopreuprim  47450  goldbachth  47471  fmtnofac1  47494  prmdvdsfmtnof1lem1  47508  lighneal  47535  grimuhgr  47815  uhgrimisgrgriclem  47835  clnbgrgrim  47839  grimedg  47840  usgrgrtrirex  47852  isubgr3stgrlem3  47870  isubgr3stgrlem6  47873  uspgrlimlem2  47891  grlimgrtri  47898  grlicsym  47908  clnbgr3stgrgrlic  47914  gpgusgralem  47945  2tceilhalfelfzo1  47952  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  uspgropssxp  47987  rngccatidALTV  48115  ringccatidALTV  48149  lcosslsp  48283  fllog2  48417  dignn0flhalf  48467  fv1arycl  48486  1arymaptf1  48491  fv2arycl  48497  2arymaptf1  48502  itschlc0yqe  48609  itsclc0xyqsol  48617  seposep  48721  iscnrm3lem6  48734  iunord  48906  setrec2fun  48922