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  1341  3exp1  1353  3expd  1354  exp5o  1356  3ecase  1476  rexlimdv3a  3159  rabssdv  4075  reupick2  4331  disjiund  5134  otiunsndisj  5525  wefrc  5679  tz7.7  6410  unizlim  6507  funimassd  6975  fvelimad  6976  fveqdmss  7098  fompt  7138  f1oiso2  7372  ssorduni  7799  sucexeloniOLD  7830  suceloniOLD  7832  tfisi  7880  resf1extb  7956  funeldmdif  8073  poxp  8153  poseq  8183  fpr3g  8310  frrlem10  8320  smo11  8404  tfrlem5  8420  odi  8617  omass  8618  nndi  8661  nnmass  8662  naddoa  8740  undifixp  8974  findcard  9203  php3  9249  ac6sfi  9320  domunfican  9361  mapfien2  9449  fisup2g  9508  fiinf2g  9540  ttrclss  9760  ttrclselem2  9766  indcardi  10081  acndom  10091  ackbij1lem16  10274  infpssrlem4  10346  fin23lem11  10357  isfin2-2  10359  fin23lem34  10386  fin1a2lem10  10449  hsmexlem2  10467  axcc3  10478  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axcclem  10497  ttukeyg  10557  axdclem2  10560  axacndlem4  10650  axacndlem5  10651  axacnd  10652  tskr1om2  10808  tskwe2  10813  tskord  10820  tskcard  10821  tskuni  10823  tskwun  10824  gruiin  10850  grudomon  10857  gruina  10858  mulcanpi  10940  adderpq  10996  mulerpq  10997  dedekindle  11425  divgt0  12136  divge0  12137  nnne0  12300  uzind  12710  uzind2  12711  iccsplit  13525  ssnn0fi  14026  expmordi  14207  sqlecan  14248  modexp  14277  expnngt1  14280  facavg  14340  2cshwcshw  14864  relexpcnv  15074  relexpaddnn  15090  relexpaddg  15092  pwdif  15904  prodfn0  15930  prodfrec  15931  ntrivcvgfvn0  15935  fprodabs  16010  bpolycl  16088  bpolydif  16091  fprodefsum  16131  dvdsmodexp  16298  dvdsaddre2b  16344  nn0rppwr  16598  dvdsnprmd  16727  2mulprm  16730  prmndvdsfaclt  16762  ncoprmlnprm  16765  fermltl  16821  pceu  16884  setsstruct2  17211  setsstruct  17213  mreexexd  17691  isglbd  18554  symgpssefmnd  19413  pmtrfrn  19476  psgnunilem4  19515  ablsimpgprmd  20135  mulgass2  20306  islss4  20960  lspsneu  21125  lspfixed  21130  lspexch  21131  lsmcv  21143  lspsolvlem  21144  rnglidlmcl  21226  xrsdsreclblem  21430  nzerooringczr  21491  isphld  21672  mdetralt  22614  mdetunilem9  22626  fiinopn  22907  neips  23121  tpnei  23129  neindisj2  23131  opnneiid  23134  hausnei2  23361  cmpsublem  23407  cmpsub  23408  cmpcld  23410  comppfsc  23540  filufint  23928  cfinufil  23936  rnelfm  23961  alexsubALTlem1  24055  alexsubALTlem4  24058  alexsubALT  24059  tsmsxp  24163  neibl  24514  tngngp3  24677  tgqioo  24821  ovolunlem2  25533  iunmbl2  25592  itg1le  25748  vieta1  26354  aannenlem2  26371  aalioulem3  26376  aalioulem4  26377  aaliou2  26382  wilthlem3  27113  bcmono  27321  gausslemma2dlem1a  27409  sslttr  27852  ssltun1  27853  ssltun2  27854  sltlpss  27945  precsexlem8  28238  precsexlem9  28239  precsex  28242  expscl  28413  expsgt0  28415  pw2cut  28420  iscgrglt  28522  axcontlem7  28985  elntg2  29000  edglnl  29160  numedglnl  29161  ausgrumgri  29184  ausgrusgri  29185  usgrausgrb  29186  usgredg2vtxeuALT  29239  ushgredgedg  29246  ushgredgedgloop  29248  nbuhgr2vtx1edgb  29369  cusgrsize2inds  29471  upgrewlkle2  29624  wlkl1loop  29656  redwlk  29690  pthdivtx  29747  pthdadjvtx  29748  upgr2pthnlp  29752  upgrspthswlk  29758  clwlkl1loop  29803  cyclnumvtx  29820  wwlksnred  29912  wwlksnextbi  29914  elwwlks2ons3im  29974  umgrwwlks2on  29977  clwwlknwwlksn  30057  clwwlkinwwlk  30059  wwlksext2clwwlk  30076  1pthon2v  30172  uhgr3cyclex  30201  n4cyclfrgr  30310  frgrwopreg  30342  numclwwlk1lem2f1  30376  clwwlknonclwlknonf1o  30381  wlkl0  30386  frgrreggt1  30412  frgrreg  30413  frgrregord013  30414  chintcli  31350  spansnss  31590  elspansn4  31592  chscllem4  31659  hoadddir  31823  adjmul  32111  kbass6  32140  spansncv2  32312  sumdmdii  32434  nexple  32833  bnj1417  35055  lfuhgr2  35124  cusgredgex  35127  sat1el2xp  35384  fmlasuc  35391  satffunlem1lem1  35407  satffunlem2lem1  35409  mclsind  35575  iprodefisumlem  35740  btwndiff  36028  elicc3  36318  finminlem  36319  sdclem2  37749  clmgmOLD  37858  grpomndo  37882  zerdivemp1x  37954  lsmsat  39009  lsmcv2  39030  lcvat  39031  lsatcveq0  39033  lcvexchlem4  39038  lcvexchlem5  39039  islshpcv  39054  l1cvpat  39055  lshpkrlem6  39116  omlfh3N  39260  cvlsupr4  39346  cvlsupr5  39347  cvlsupr6  39348  2llnneN  39411  hlrelat3  39414  cvrval3  39415  cvrval4N  39416  cvrexchlem  39421  2atlt  39441  cvrat4  39445  atbtwnexOLDN  39449  atbtwnex  39450  athgt  39458  3dim1  39469  3dim2  39470  3dim3  39471  1cvratex  39475  llnle  39520  atcvrlln2  39521  atcvrlln  39522  2llnmat  39526  lplnle  39542  lplnnle2at  39543  lplnnlelln  39545  llncvrlpln2  39559  2llnjN  39569  lvoli2  39583  lvolnlelln  39586  lvolnlelpln  39587  4atlem10  39608  4atlem11  39611  4atlem12  39614  lplncvrlvol2  39617  2lplnj  39622  lneq2at  39780  lnatexN  39781  lnjatN  39782  lncvrat  39784  2lnat  39786  cdlemb  39796  paddasslem14  39835  llnexchb2  39871  dalawlem10  39882  dalawlem13  39885  dalawlem14  39886  dalaw  39888  pclclN  39893  pclfinN  39902  osumcllem11N  39968  lhp2lt  40003  lhpexle3lem  40013  4atexlem7  40077  ldilcnv  40117  ldilco  40118  ltrncnv  40148  trlval2  40165  cdleme24  40354  cdleme26ee  40362  cdleme28  40375  cdleme32le  40449  cdleme50trn2  40553  cdleme50ltrn  40559  cdleme  40562  cdlemf1  40563  cdlemf  40565  cdlemg1cex  40590  cdlemg2ce  40594  cdlemg18b  40681  ltrnco  40721  tendocan  40826  cdlemk28-3  40910  cdlemk11t  40948  dia2dimlem6  41071  dia2dimlem12  41077  dihlsscpre  41236  dihord4  41260  dihord5b  41261  dihmeetlem3N  41307  dihmeetlem20N  41328  dvh4dimlem  41445  lclkrlem2y  41533  mapdpglem24  41706  mapdpglem32  41707  mapdpg  41708  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  mapdh9a  41791  mapdh9aOLDN  41792  hdmap14lem6  41875  hdmapglem7  41931  indstrd  42194  nnadddir  42305  nnmulcom  42307  sn-addlid  42434  remulcand  42468  mzpexpmpt  42756  pellexlem5  42844  pellex  42846  pell14qrexpclnn0  42877  pellfundex  42897  monotuz  42953  monotoddzzfi  42954  rmxypos  42959  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  jm2.19lem3  43003  jm2.15nn0  43015  jm2.16nn0  43016  aomclem2  43067  aomclem6  43071  dfac11  43074  hbtlem5  43140  cnsrexpcl  43177  cantnf2  43338  dflim5  43342  relexpxpnnidm  43716  relexpiidm  43717  relexpss1d  43718  iunrelexpmin1  43721  relexpmulnn  43722  iunrelexpmin2  43725  relexp01min  43726  relexp0a  43729  relexpxpmin  43730  relexpaddss  43731  trclimalb2  43739  tfindsd  44224  3impexpbicomi  44501  ee333  44527  eel12131  44733  eel2122old  44738  e333  44753  ordelordALTVD  44887  refsumcn  45035  uzwo4  45058  ssinc  45092  ssdec  45093  iunincfi  45099  restuni3  45123  eliuniin2  45125  rabssd  45147  reximdd  45153  suprnmpt  45179  disjf1o  45196  disjinfi  45197  ssnnf1octb  45199  choicefi  45205  mapssbi  45218  unirnmapsn  45219  iunmapsn  45222  rnmptlb  45250  rnmptbddlem  45251  infnsuprnmpt  45257  fperiodmullem  45315  upbdrech  45317  ssfiunibd  45321  supxrgere  45344  iuneqfzuzlem  45345  supxrgelem  45348  supxrge  45349  suplesup  45350  infrpge  45362  infleinf  45383  suplesup2  45387  supxrunb3  45410  infleinf2  45425  rexabslelem  45429  infrnmptle  45434  infxrunb3rnmpt  45439  iccshift  45531  iooshift  45535  fmul01  45595  fmuldfeq  45598  fmul01lt1  45601  mullimc  45631  islptre  45634  mullimcf  45638  limcperiod  45643  islpcn  45654  limsupre  45656  limcleqr  45659  neglimc  45662  addlimc  45663  0ellimcdiv  45664  limclner  45666  fnlimfvre  45689  limsuppnflem  45725  limsupmnfuzlem  45741  limsupre3lem  45747  limsupre3uzlem  45750  climuzlem  45758  limsupgtlem  45792  coskpi2  45881  cosknegpi  45884  cncfshift  45889  cncfperiod  45894  icccncfext  45902  dvnmptdivc  45953  dvnmptconst  45956  dvnmul  45958  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  iblspltprt  45988  itgspltprt  45994  itgperiod  45996  ismbl3  46001  stoweidlem3  46018  stoweidlem31  46046  stoweidlem59  46074  stirlinglem13  46101  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem51  46172  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem80  46201  fourierdlem81  46202  fourierdlem89  46210  fourierdlem91  46212  fourierdlem93  46214  fourierdlem97  46218  elaa2  46249  qndenserrnopnlem  46312  salexct  46349  subsaliuncl  46373  subsalsal  46374  sge0tsms  46395  sge0f1o  46397  sge0fsum  46402  sge0supre  46404  sge0sup  46406  sge0rnbnd  46408  sge0gerp  46410  sge0pnffigt  46411  sge0lefi  46413  sge0ltfirp  46415  sge0resrn  46419  sge0resplit  46421  sge0split  46424  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0rpcpnf  46436  sge0isum  46442  sge0xp  46444  sge0xaddlem2  46449  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  nnfoctbdjlem  46470  nnfoctbdj  46471  iundjiun  46475  meadjiunlem  46480  voliunsge0lem  46487  meaiuninclem  46495  meaiininc2  46503  carageniuncllem1  46536  carageniuncllem2  46537  caratheodorylem1  46541  caratheodorylem2  46542  isomenndlem  46545  ovnsupge0  46572  ovnlerp  46577  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmvval0  46602  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem2  46617  opnvonmbllem2  46648  ovnovollem3  46673  vonioo  46697  vonicc  46700  pimiooltgt  46725  sssmf  46753  smfaddlem1  46778  smflimlem6  46791  smfmullem4  46809  smfpimbor1lem1  46813  smfco  46817  smfpimcc  46823  smflimmpt  46825  smfinflem  46832  smflimsuplem7  46841  smflimsuplem8  46842  smflimsupmpt  46844  smfliminfmpt  46847  cfsetsnfsetf1  47071  elsetpreimafveqfv  47379  iccpartiltu  47409  sprsymrelfvlem  47477  reuopreuprim  47513  goldbachth  47534  fmtnofac1  47557  prmdvdsfmtnof1lem1  47571  lighneal  47598  grimuhgr  47878  uhgrimisgrgriclem  47898  clnbgrgrim  47902  grimedg  47903  usgrgrtrirex  47917  isubgr3stgrlem3  47935  isubgr3stgrlem6  47938  uspgrlimlem2  47956  grlimgrtri  47963  grlicsym  47973  clnbgr3stgrgrlic  47979  gpgusgralem  48011  2tceilhalfelfzo1  48018  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  uspgropssxp  48060  rngccatidALTV  48188  ringccatidALTV  48222  lcosslsp  48355  fllog2  48489  dignn0flhalf  48539  fv1arycl  48558  1arymaptf1  48563  fv2arycl  48569  2arymaptf1  48574  itschlc0yqe  48681  itsclc0xyqsol  48689  seposep  48823  iscnrm3lem6  48835  iunord  49195  setrec2fun  49211