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 425	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expb  1138  3expib  1140  3com12  1141  3com13  1142  pm3.2an3  1359  3exp1  1371  3expd  1372  exp5o  1374  3ecase  1505  rexlimdv3a  3167  rabssdv  4022  reupick2  4277  disjiund  5094  otiunsndisj  5497  wefrc  5649  tz7.7  6383  unizlim  6482  funimassd  6944  fvelimad  6945  fveqdmss  7071  fompt  7111  f1resrcmplf1d  7272  f1oiso2  7353  ssorduni  7778  tfisi  7855  resf1extb  7931  funeldmdif  8045  poxp  8126  poseq  8156  fpr3g  8284  frrlem10  8294  smo11  8353  tfrlem5  8368  odi  8566  omass  8567  nndi  8611  nnmass  8612  naddoa  8691  undifixp  8941  findcard  9158  php3  9203  ac6sfi  9254  domunfican  9291  mapfien2  9379  fisup2g  9439  fiinf2g  9472  ttrclss  9699  ttrclselem2  9705  indcardi  10044  acndom  10054  ackbij1lem16  10236  infpssrlem4  10308  fin23lem11  10319  isfin2-2  10321  fin23lem34  10348  fin1a2lem10  10411  hsmexlem2  10429  axcc3  10440  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  axcclem  10459  ttukeyg  10519  axdclem2  10522  axacndlem4  10619  axacndlem5  10620  axacnd  10621  tskr1om2  10777  tskwe2  10782  tskord  10789  tskcard  10790  tskuni  10792  tskwun  10793  gruiin  10819  grudomon  10826  gruina  10827  mulcanpi  10909  adderpq  10965  mulerpq  10966  dedekindle  11398  divgt0  12107  divge0  12108  nnne0  12294  nnadddir  12316  nnmulcom  12318  uzind  12713  uzind2  12714  iccsplit  13538  ssnn0fi  14049  expmordi  14231  sqlecan  14273  modexp  14302  expnngt1  14305  facavg  14365  2cshwcshw  14896  relexpcnv  15108  relexpaddnn  15124  relexpaddg  15126  pwdif  15957  prodfn0  15983  prodfrec  15984  ntrivcvgfvn0  15988  fprodabs  16061  bpolycl  16138  bpolydif  16141  fprodefsum  16181  dvdsmodexp  16350  dvdsaddre2b  16397  nn0rppwr  16651  dvdsnprmd  16780  2mulprm  16783  prmndvdsfaclt  16816  ncoprmlnprm  16819  fermltl  16875  pceu  16938  setsstruct2  17266  setsstruct  17268  mreexexd  17736  isglbd  18597  symgpssefmnd  19523  pmtrfrn  19585  psgnunilem4  19624  ablsimpgprmd  20244  mulgass2  20451  islss4  21146  lspsneu  21310  lspfixed  21315  lspexch  21316  lsmcv  21328  lspsolvlem  21329  rnglidlmcl  21404  unichnlidl  21425  xrsdsreclblem  21626  nzerooringczr  21693  isphld  21867  mdetralt  22830  mdetunilem9  22842  fiinopn  23126  neips  23338  tpnei  23346  neindisj2  23348  opnneiid  23351  hausnei2  23578  cmpsublem  23624  cmpsub  23625  cmpcld  23627  comppfsc  23758  filufint  24146  cfinufil  24154  rnelfm  24179  alexsubALTlem1  24273  alexsubALTlem4  24276  alexsubALT  24277  tsmsxp  24381  neibl  24727  tngngp3  24882  tgqioo  25026  ovolunlem2  25726  iunmbl2  25785  itg1le  25941  vieta1  26544  aannenlem2  26565  aalioulem3  26570  aalioulem4  26571  aaliou2  26576  wilthlem3  27306  bcmono  27513  gausslemma2dlem1a  27601  sltstr  28052  sltsun1  28053  sltsun2  28054  ltslpss  28173  precsexlem8  28479  precsexlem9  28480  precsex  28483  onsfi  28621  oldfib  28642  expscllem  28695  expsgt0  28702  pw2cut  28725  pw2cut2  28727  bdaypw2n0bnd  28729  bdayfin  28752  iscgrglt  28856  axcontlem7  29427  elntg2  29442  edglnl  29600  numedglnl  29601  lfuhgr2  29606  ausgrumgri  29627  ausgrusgri  29628  usgrausgrb  29629  usgredg2vtxeuALT  29682  ushgredgedg  29689  ushgredgedgloop  29691  nbuhgr2vtx1edgb  29812  cusgrsize2inds  29913  upgrewlkle2  30066  wlkl1loop  30097  redwlk  30130  pthdivtx  30191  pthdadjvtx  30192  upgr2pthnlp  30197  upgrspthswlk  30203  clwlkl1loop  30249  cyclnumvtx  30267  wwlksnred  30360  wwlksnextbi  30362  elwwlks2ons3im  30422  usgrwwlks2on  30426  umgrwwlks2on  30427  clwwlknwwlksn  30508  clwwlkinwwlk  30510  wwlksext2clwwlk  30527  1pthon2v  30633  uhgr3cyclex  30662  n4cyclfrgr  30771  frgrwopreg  30803  numclwwlk1lem2f1  30837  clwwlknonclwlknonf1o  30842  wlkl0  30847  frgrreggt1  30873  frgrreg  30874  frgrregord013  30875  chintcli  31812  spansnss  32052  elspansn4  32054  chscllem4  32121  hoadddir  32285  adjmul  32573  kbass6  32602  spansncv2  32774  sumdmdii  32896  nexple  33303  bnj1417  35550  cusgredgex  35720  sat1el2xp  35958  fmlasuc  35965  satffunlem1lem1  35981  satffunlem2lem1  35983  mclsind  36149  iprodefisumlem  36319  btwndiff  36607  elicc3  36936  finminlem  36937  axtcond  37097  ttcmin  37115  sdclem2  38492  clmgmOLD  38601  grpomndo  38625  zerdivemp1x  38697  lsmsat  39881  lsmcv2  39902  lcvat  39903  lsatcveq0  39905  lcvexchlem4  39910  lcvexchlem5  39911  islshpcv  39926  l1cvpat  39927  lshpkrlem6  39988  omlfh3N  40132  cvlsupr4  40218  cvlsupr5  40219  cvlsupr6  40220  2llnneN  40282  hlrelat3  40285  cvrval3  40286  cvrval4N  40287  cvrexchlem  40292  2atlt  40312  cvrat4  40316  atbtwnexOLDN  40320  atbtwnex  40321  athgt  40329  3dim1  40340  3dim2  40341  3dim3  40342  1cvratex  40346  llnle  40391  atcvrlln2  40392  atcvrlln  40393  2llnmat  40397  lplnle  40413  lplnnle2at  40414  lplnnlelln  40416  llncvrlpln2  40430  2llnjN  40440  lvoli2  40454  lvolnlelln  40457  lvolnlelpln  40458  4atlem10  40479  4atlem11  40482  4atlem12  40485  lplncvrlvol2  40488  2lplnj  40493  lneq2at  40651  lnatexN  40652  lnjatN  40653  lncvrat  40655  2lnat  40657  cdlemb  40667  paddasslem14  40706  llnexchb2  40742  dalawlem10  40753  dalawlem13  40756  dalawlem14  40757  dalaw  40759  pclclN  40764  pclfinN  40773  osumcllem11N  40839  lhp2lt  40874  lhpexle3lem  40884  4atexlem7  40948  ldilcnv  40988  ldilco  40989  ltrncnv  41019  trlval2  41036  cdleme24  41225  cdleme26ee  41233  cdleme28  41246  cdleme32le  41320  cdleme50trn2  41424  cdleme50ltrn  41430  cdleme  41433  cdlemf1  41434  cdlemf  41436  cdlemg1cex  41461  cdlemg2ce  41465  cdlemg18b  41552  ltrnco  41592  tendocan  41697  cdlemk28-3  41781  cdlemk11t  41819  dia2dimlem6  41942  dia2dimlem12  41948  dihlsscpre  42107  dihord4  42131  dihord5b  42132  dihmeetlem3N  42178  dihmeetlem20N  42199  dvh4dimlem  42316  lclkrlem2y  42404  mapdpglem24  42577  mapdpglem32  42578  mapdpg  42579  baerlem3lem2  42583  baerlem5alem2  42584  baerlem5blem2  42585  mapdh9a  42662  mapdh9aOLDN  42663  hdmap14lem6  42746  hdmapglem7  42802  indstrd  43059  sn-addlid  43279  remulcand  43314  mzpexpmpt  43590  pellexlem5  43674  pellex  43676  pell14qrexpclnn0  43707  pellfundex  43727  monotuz  43782  monotoddzzfi  43783  rmxypos  43788  jm2.17a  43801  jm2.17b  43802  rmygeid  43805  jm2.19lem3  43832  jm2.15nn0  43844  jm2.16nn0  43845  aomclem2  43896  aomclem6  43900  dfac11  43903  hbtlem5  43969  cnsrexpcl  44006  cantnf2  44166  dflim5  44170  relexpxpnnidm  44543  relexpiidm  44544  relexpss1d  44545  iunrelexpmin1  44548  relexpmulnn  44549  iunrelexpmin2  44552  relexp01min  44553  relexp0a  44556  relexpxpmin  44557  relexpaddss  44558  trclimalb2  44566  tfindsd  45048  3impexpbicomi  45304  ee333  45330  eel12131  45535  eel2122old  45540  e333  45555  ordelordALTVD  45689  refsumcn  45864  uzwo4  45887  ssinc  45919  ssdec  45920  iunincfi  45926  restuni3  45950  eliuniin2  45952  rabssd  45974  reximdd  45980  suprnmpt  46006  disjf1o  46023  disjinfi  46024  ssnnf1octb  46026  choicefi  46031  mapssbi  46043  unirnmapsn  46044  iunmapsn  46047  rnmptlb  46072  rnmptbddlem  46073  infnsuprnmpt  46079  fperiodmullem  46136  upbdrech  46138  ssfiunibd  46142  supxrgere  46163  iuneqfzuzlem  46164  supxrgelem  46167  supxrge  46168  suplesup  46169  infrpge  46181  infleinf  46201  suplesup2  46205  supxrunb3  46228  infleinf2  46242  rexabslelem  46246  infrnmptle  46251  infxrunb3rnmpt  46256  iccshift  46348  iooshift  46352  fmul01  46410  fmuldfeq  46413  fmul01lt1  46416  mullimc  46446  islptre  46449  mullimcf  46453  limcperiod  46458  islpcn  46467  limsupre  46469  limcleqr  46472  neglimc  46475  addlimc  46476  0ellimcdiv  46477  limclner  46479  fnlimfvre  46502  limsuppnflem  46538  limsupmnfuzlem  46554  limsupre3lem  46560  limsupre3uzlem  46563  climuzlem  46571  limsupgtlem  46605  coskpi2  46694  cosknegpi  46697  cncfshift  46702  cncfperiod  46707  icccncfext  46715  dvnmptdivc  46766  dvnmptconst  46769  dvnmul  46771  dvmptfprodlem  46772  dvmptfprod  46773  dvnprodlem1  46774  dvnprodlem2  46775  iblspltprt  46801  itgspltprt  46807  itgperiod  46809  ismbl3  46814  stoweidlem3  46831  stoweidlem31  46859  stoweidlem59  46887  stirlinglem13  46914  fourierdlem41  46976  fourierdlem42  46977  fourierdlem48  46982  fourierdlem51  46985  fourierdlem70  47004  fourierdlem71  47005  fourierdlem73  47007  fourierdlem80  47014  fourierdlem81  47015  fourierdlem89  47023  fourierdlem91  47025  fourierdlem93  47027  fourierdlem97  47031  elaa2  47062  qndenserrnopnlem  47125  salexct  47162  subsaliuncl  47186  subsalsal  47187  sge0tsms  47208  sge0f1o  47210  sge0fsum  47215  sge0supre  47217  sge0sup  47219  sge0rnbnd  47221  sge0gerp  47223  sge0pnffigt  47224  sge0lefi  47226  sge0ltfirp  47228  sge0resrn  47232  sge0resplit  47234  sge0split  47237  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  sge0rpcpnf  47249  sge0isum  47255  sge0xp  47257  sge0xaddlem2  47262  sge0uzfsumgt  47272  sge0seq  47274  sge0reuz  47275  nnfoctbdjlem  47283  nnfoctbdj  47284  iundjiun  47288  meadjiunlem  47293  voliunsge0lem  47300  meaiuninclem  47308  meaiininc2  47316  carageniuncllem1  47349  carageniuncllem2  47350  caratheodorylem1  47354  caratheodorylem2  47355  isomenndlem  47358  ovnsupge0  47385  ovnlerp  47390  ovncvrrp  47392  ovnsubaddlem1  47398  hoidmvval0  47415  hoidmv1lelem3  47421  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  ovnhoilem2  47430  opnvonmbllem2  47461  ovnovollem3  47486  vonioo  47510  vonicc  47513  pimiooltgt  47538  smfaddlem1  47591  smflimlem6  47604  smfmullem4  47622  smfpimbor1lem1  47626  smfco  47630  smfpimcc  47636  smflimmpt  47638  smfinflem  47645  smflimsuplem7  47654  smflimsuplem8  47655  smflimsupmpt  47657  smfliminfmpt  47660  cfsetsnfsetf1  47947  nnmul2b  48219  2tceilhalfelfzo1  48224  elsetpreimafveqfv  48292  iccpartiltu  48322  sprsymrelfvlem  48390  reuopreuprim  48426  nprmmul2  48428  goldbachth  48450  fmtnofac1  48473  prmdvdsfmtnof1lem1  48487  lighneal  48514  grimuhgr  48803  uhgrimedgi  48806  uhgrimisgrgriclem  48846  clnbgrgrim  48850  grimedg  48851  usgrgrtrirex  48866  isubgr3stgrlem3  48884  isubgr3stgrlem6  48887  uspgrlimlem2  48905  grlimgrtri  48919  grlicsym  48929  clnbgr3stgrgrlic  48936  gpgusgralem  48972  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  uspgropssxp  49060  rngccatidALTV  49187  ringccatidALTV  49221  lcosslsp  49368  fllog2  49498  dignn0flhalf  49548  fv1arycl  49567  1arymaptf1  49572  fv2arycl  49578  2arymaptf1  49583  itschlc0yqe  49690  itsclc0xyqsol  49698  seposep  49852  iscnrm3lem6  49864  iunord  50602  setrec2fun  50618