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  3143  rabssdv  4028  reupick2  4285  disjiund  5091  otiunsndisj  5476  wefrc  5626  tz7.7  6351  unizlim  6449  funimassd  6908  fvelimad  6909  fveqdmss  7032  fompt  7072  f1oiso2  7308  ssorduni  7734  tfisi  7811  resf1extb  7886  funeldmdif  8002  poxp  8080  poseq  8110  fpr3g  8237  frrlem10  8247  smo11  8306  tfrlem5  8321  odi  8516  omass  8517  nndi  8561  nnmass  8562  naddoa  8640  undifixp  8884  findcard  9100  php3  9145  ac6sfi  9196  domunfican  9234  mapfien2  9324  fisup2g  9384  fiinf2g  9417  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  11309  divgt0  12022  divge0  12023  nnne0  12191  uzind  12596  uzind2  12597  iccsplit  13413  ssnn0fi  13920  expmordi  14102  sqlecan  14144  modexp  14173  expnngt1  14176  facavg  14236  2cshwcshw  14760  relexpcnv  14970  relexpaddnn  14986  relexpaddg  14988  pwdif  15803  prodfn0  15829  prodfrec  15830  ntrivcvgfvn0  15834  fprodabs  15909  bpolycl  15987  bpolydif  15990  fprodefsum  16030  dvdsmodexp  16199  dvdsaddre2b  16246  nn0rppwr  16500  dvdsnprmd  16629  2mulprm  16632  prmndvdsfaclt  16664  ncoprmlnprm  16667  fermltl  16723  pceu  16786  setsstruct2  17113  setsstruct  17115  mreexexd  17583  isglbd  18444  symgpssefmnd  19337  pmtrfrn  19399  psgnunilem4  19438  ablsimpgprmd  20058  mulgass2  20256  islss4  20925  lspsneu  21090  lspfixed  21095  lspexch  21096  lsmcv  21108  lspsolvlem  21109  rnglidlmcl  21183  xrsdsreclblem  21379  nzerooringczr  21447  isphld  21621  mdetralt  22564  mdetunilem9  22576  fiinopn  22857  neips  23069  tpnei  23077  neindisj2  23079  opnneiid  23082  hausnei2  23309  cmpsublem  23355  cmpsub  23356  cmpcld  23358  comppfsc  23488  filufint  23876  cfinufil  23884  rnelfm  23909  alexsubALTlem1  24003  alexsubALTlem4  24006  alexsubALT  24007  tsmsxp  24111  neibl  24457  tngngp3  24612  tgqioo  24756  ovolunlem2  25467  iunmbl2  25526  itg1le  25682  vieta1  26288  aannenlem2  26305  aalioulem3  26310  aalioulem4  26311  aaliou2  26316  wilthlem3  27048  bcmono  27256  gausslemma2dlem1a  27344  sltstr  27795  sltsun1  27796  sltsun2  27797  ltslpss  27916  precsexlem8  28222  precsexlem9  28223  precsex  28226  onsfi  28364  oldfib  28385  expscllem  28438  expsgt0  28445  pw2cut  28468  pw2cut2  28470  bdaypw2n0bnd  28472  bdayfin  28495  iscgrglt  28598  axcontlem7  29055  elntg2  29070  edglnl  29228  numedglnl  29229  ausgrumgri  29252  ausgrusgri  29253  usgrausgrb  29254  usgredg2vtxeuALT  29307  ushgredgedg  29314  ushgredgedgloop  29316  nbuhgr2vtx1edgb  29437  cusgrsize2inds  29539  upgrewlkle2  29692  wlkl1loop  29723  redwlk  29756  pthdivtx  29812  pthdadjvtx  29813  upgr2pthnlp  29817  upgrspthswlk  29823  clwlkl1loop  29868  cyclnumvtx  29885  wwlksnred  29977  wwlksnextbi  29979  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  clwwlknwwlksn  30125  clwwlkinwwlk  30127  wwlksext2clwwlk  30144  1pthon2v  30240  uhgr3cyclex  30269  n4cyclfrgr  30378  frgrwopreg  30410  numclwwlk1lem2f1  30444  clwwlknonclwlknonf1o  30449  wlkl0  30454  frgrreggt1  30480  frgrreg  30481  frgrregord013  30482  chintcli  31419  spansnss  31659  elspansn4  31661  chscllem4  31728  hoadddir  31892  adjmul  32180  kbass6  32209  spansncv2  32381  sumdmdii  32503  nexple  32936  bnj1417  35217  lfuhgr2  35335  cusgredgex  35338  sat1el2xp  35595  fmlasuc  35602  satffunlem1lem1  35618  satffunlem2lem1  35620  mclsind  35786  iprodefisumlem  35956  btwndiff  36243  elicc3  36533  finminlem  36534  sdclem2  37993  clmgmOLD  38102  grpomndo  38126  zerdivemp1x  38198  lsmsat  39384  lsmcv2  39405  lcvat  39406  lsatcveq0  39408  lcvexchlem4  39413  lcvexchlem5  39414  islshpcv  39429  l1cvpat  39430  lshpkrlem6  39491  omlfh3N  39635  cvlsupr4  39721  cvlsupr5  39722  cvlsupr6  39723  2llnneN  39785  hlrelat3  39788  cvrval3  39789  cvrval4N  39790  cvrexchlem  39795  2atlt  39815  cvrat4  39819  atbtwnexOLDN  39823  atbtwnex  39824  athgt  39832  3dim1  39843  3dim2  39844  3dim3  39845  1cvratex  39849  llnle  39894  atcvrlln2  39895  atcvrlln  39896  2llnmat  39900  lplnle  39916  lplnnle2at  39917  lplnnlelln  39919  llncvrlpln2  39933  2llnjN  39943  lvoli2  39957  lvolnlelln  39960  lvolnlelpln  39961  4atlem10  39982  4atlem11  39985  4atlem12  39988  lplncvrlvol2  39991  2lplnj  39996  lneq2at  40154  lnatexN  40155  lnjatN  40156  lncvrat  40158  2lnat  40160  cdlemb  40170  paddasslem14  40209  llnexchb2  40245  dalawlem10  40256  dalawlem13  40259  dalawlem14  40260  dalaw  40262  pclclN  40267  pclfinN  40276  osumcllem11N  40342  lhp2lt  40377  lhpexle3lem  40387  4atexlem7  40451  ldilcnv  40491  ldilco  40492  ltrncnv  40522  trlval2  40539  cdleme24  40728  cdleme26ee  40736  cdleme28  40749  cdleme32le  40823  cdleme50trn2  40927  cdleme50ltrn  40933  cdleme  40936  cdlemf1  40937  cdlemf  40939  cdlemg1cex  40964  cdlemg2ce  40968  cdlemg18b  41055  ltrnco  41095  tendocan  41200  cdlemk28-3  41284  cdlemk11t  41322  dia2dimlem6  41445  dia2dimlem12  41451  dihlsscpre  41610  dihord4  41634  dihord5b  41635  dihmeetlem3N  41681  dihmeetlem20N  41702  dvh4dimlem  41819  lclkrlem2y  41907  mapdpglem24  42080  mapdpglem32  42081  mapdpg  42082  baerlem3lem2  42086  baerlem5alem2  42087  baerlem5blem2  42088  mapdh9a  42165  mapdh9aOLDN  42166  hdmap14lem6  42249  hdmapglem7  42305  indstrd  42563  nnadddir  42640  nnmulcom  42642  sn-addlid  42774  remulcand  42809  mzpexpmpt  43102  pellexlem5  43190  pellex  43192  pell14qrexpclnn0  43223  pellfundex  43243  monotuz  43298  monotoddzzfi  43299  rmxypos  43304  jm2.17a  43317  jm2.17b  43318  rmygeid  43321  jm2.19lem3  43348  jm2.15nn0  43360  jm2.16nn0  43361  aomclem2  43412  aomclem6  43416  dfac11  43419  hbtlem5  43485  cnsrexpcl  43522  cantnf2  43682  dflim5  43686  relexpxpnnidm  44059  relexpiidm  44060  relexpss1d  44061  iunrelexpmin1  44064  relexpmulnn  44065  iunrelexpmin2  44068  relexp01min  44069  relexp0a  44072  relexpxpmin  44073  relexpaddss  44074  trclimalb2  44082  tfindsd  44566  3impexpbicomi  44837  ee333  44863  eel12131  45068  eel2122old  45073  e333  45088  ordelordALTVD  45222  refsumcn  45390  uzwo4  45413  ssinc  45446  ssdec  45447  iunincfi  45453  restuni3  45477  eliuniin2  45479  rabssd  45501  reximdd  45507  suprnmpt  45533  disjf1o  45550  disjinfi  45551  ssnnf1octb  45553  choicefi  45558  mapssbi  45571  unirnmapsn  45572  iunmapsn  45575  rnmptlb  45601  rnmptbddlem  45602  infnsuprnmpt  45608  fperiodmullem  45665  upbdrech  45667  ssfiunibd  45671  supxrgere  45692  iuneqfzuzlem  45693  supxrgelem  45696  supxrge  45697  suplesup  45698  infrpge  45710  infleinf  45730  suplesup2  45734  supxrunb3  45757  infleinf2  45772  rexabslelem  45776  infrnmptle  45781  infxrunb3rnmpt  45786  iccshift  45878  iooshift  45882  fmul01  45940  fmuldfeq  45943  fmul01lt1  45946  mullimc  45976  islptre  45979  mullimcf  45983  limcperiod  45988  islpcn  45997  limsupre  45999  limcleqr  46002  neglimc  46005  addlimc  46006  0ellimcdiv  46007  limclner  46009  fnlimfvre  46032  limsuppnflem  46068  limsupmnfuzlem  46084  limsupre3lem  46090  limsupre3uzlem  46093  climuzlem  46101  limsupgtlem  46135  coskpi2  46224  cosknegpi  46227  cncfshift  46232  cncfperiod  46237  icccncfext  46245  dvnmptdivc  46296  dvnmptconst  46299  dvnmul  46301  dvmptfprodlem  46302  dvmptfprod  46303  dvnprodlem1  46304  dvnprodlem2  46305  iblspltprt  46331  itgspltprt  46337  itgperiod  46339  ismbl3  46344  stoweidlem3  46361  stoweidlem31  46389  stoweidlem59  46417  stirlinglem13  46444  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem51  46515  fourierdlem70  46534  fourierdlem71  46535  fourierdlem73  46537  fourierdlem80  46544  fourierdlem81  46545  fourierdlem89  46553  fourierdlem91  46555  fourierdlem93  46557  fourierdlem97  46561  elaa2  46592  qndenserrnopnlem  46655  salexct  46692  subsaliuncl  46716  subsalsal  46717  sge0tsms  46738  sge0f1o  46740  sge0fsum  46745  sge0supre  46747  sge0sup  46749  sge0rnbnd  46751  sge0gerp  46753  sge0pnffigt  46754  sge0lefi  46756  sge0ltfirp  46758  sge0resrn  46762  sge0resplit  46764  sge0split  46767  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0iunmpt  46776  sge0rpcpnf  46779  sge0isum  46785  sge0xp  46787  sge0xaddlem2  46792  sge0uzfsumgt  46802  sge0seq  46804  sge0reuz  46805  nnfoctbdjlem  46813  nnfoctbdj  46814  iundjiun  46818  meadjiunlem  46823  voliunsge0lem  46830  meaiuninclem  46838  meaiininc2  46846  carageniuncllem1  46879  carageniuncllem2  46880  caratheodorylem1  46884  caratheodorylem2  46885  isomenndlem  46888  ovnsupge0  46915  ovnlerp  46920  ovncvrrp  46922  ovnsubaddlem1  46928  hoidmvval0  46945  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  ovnhoilem2  46960  opnvonmbllem2  46991  ovnovollem3  47016  vonioo  47040  vonicc  47043  pimiooltgt  47068  sssmf  47096  smfaddlem1  47121  smflimlem6  47134  smfmullem4  47152  smfpimbor1lem1  47156  smfco  47160  smfpimcc  47166  smflimmpt  47168  smfinflem  47175  smflimsuplem7  47184  smflimsuplem8  47185  smflimsupmpt  47187  smfliminfmpt  47190  cfsetsnfsetf1  47419  2tceilhalfelfzo1  47692  elsetpreimafveqfv  47752  iccpartiltu  47782  sprsymrelfvlem  47850  reuopreuprim  47886  goldbachth  47907  fmtnofac1  47930  prmdvdsfmtnof1lem1  47944  lighneal  47971  grimuhgr  48247  uhgrimedgi  48250  uhgrimisgrgriclem  48290  clnbgrgrim  48294  grimedg  48295  usgrgrtrirex  48310  isubgr3stgrlem3  48328  isubgr3stgrlem6  48331  uspgrlimlem2  48349  grlimgrtri  48363  grlicsym  48373  clnbgr3stgrgrlic  48380  gpgusgralem  48416  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  uspgropssxp  48504  rngccatidALTV  48632  ringccatidALTV  48666  lcosslsp  48798  fllog2  48928  dignn0flhalf  48978  fv1arycl  48997  1arymaptf1  49002  fv2arycl  49008  2arymaptf1  49013  itschlc0yqe  49120  itsclc0xyqsol  49128  seposep  49285  iscnrm3lem6  49297  iunord  50035  setrec2fun  50051