Theorem 3exp 1119

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 1118	. 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  1120  3expib  1122  3com12  1123  3com13  1124  pm3.2an3  1341  3exp1  1353  3expd  1354  exp5o  1356  3ecase  1476  rexlimdv3a  3138  rabssdv  4038  reupick2  4294  disjiund  5098  otiunsndisj  5480  wefrc  5632  tz7.7  6358  unizlim  6457  funimassd  6927  fvelimad  6928  fveqdmss  7050  fompt  7090  f1oiso2  7327  ssorduni  7755  sucexeloniOLD  7786  tfisi  7835  resf1extb  7910  funeldmdif  8027  poxp  8107  poseq  8137  fpr3g  8264  frrlem10  8274  smo11  8333  tfrlem5  8348  odi  8543  omass  8544  nndi  8587  nnmass  8588  naddoa  8666  undifixp  8907  findcard  9127  php3  9173  ac6sfi  9231  domunfican  9272  mapfien2  9360  fisup2g  9420  fiinf2g  9453  ttrclss  9673  ttrclselem2  9679  indcardi  9994  acndom  10004  ackbij1lem16  10187  infpssrlem4  10259  fin23lem11  10270  isfin2-2  10272  fin23lem34  10299  fin1a2lem10  10362  hsmexlem2  10380  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axcclem  10410  ttukeyg  10470  axdclem2  10473  axacndlem4  10563  axacndlem5  10564  axacnd  10565  tskr1om2  10721  tskwe2  10726  tskord  10733  tskcard  10734  tskuni  10736  tskwun  10737  gruiin  10763  grudomon  10770  gruina  10771  mulcanpi  10853  adderpq  10909  mulerpq  10910  dedekindle  11338  divgt0  12051  divge0  12052  nnne0  12220  uzind  12626  uzind2  12627  iccsplit  13446  ssnn0fi  13950  expmordi  14132  sqlecan  14174  modexp  14203  expnngt1  14206  facavg  14266  2cshwcshw  14791  relexpcnv  15001  relexpaddnn  15017  relexpaddg  15019  pwdif  15834  prodfn0  15860  prodfrec  15861  ntrivcvgfvn0  15865  fprodabs  15940  bpolycl  16018  bpolydif  16021  fprodefsum  16061  dvdsmodexp  16230  dvdsaddre2b  16277  nn0rppwr  16531  dvdsnprmd  16660  2mulprm  16663  prmndvdsfaclt  16695  ncoprmlnprm  16698  fermltl  16754  pceu  16817  setsstruct2  17144  setsstruct  17146  mreexexd  17609  isglbd  18468  symgpssefmnd  19326  pmtrfrn  19388  psgnunilem4  19427  ablsimpgprmd  20047  mulgass2  20218  islss4  20868  lspsneu  21033  lspfixed  21038  lspexch  21039  lsmcv  21051  lspsolvlem  21052  rnglidlmcl  21126  xrsdsreclblem  21329  nzerooringczr  21390  isphld  21563  mdetralt  22495  mdetunilem9  22507  fiinopn  22788  neips  23000  tpnei  23008  neindisj2  23010  opnneiid  23013  hausnei2  23240  cmpsublem  23286  cmpsub  23287  cmpcld  23289  comppfsc  23419  filufint  23807  cfinufil  23815  rnelfm  23840  alexsubALTlem1  23934  alexsubALTlem4  23937  alexsubALT  23938  tsmsxp  24042  neibl  24389  tngngp3  24544  tgqioo  24688  ovolunlem2  25399  iunmbl2  25458  itg1le  25614  vieta1  26220  aannenlem2  26237  aalioulem3  26242  aalioulem4  26243  aaliou2  26248  wilthlem3  26980  bcmono  27188  gausslemma2dlem1a  27276  sslttr  27719  ssltun1  27720  ssltun2  27721  sltlpss  27819  precsexlem8  28116  precsexlem9  28117  precsex  28120  onsfi  28247  expscllem  28316  expsgt0  28322  pw2cut  28335  iscgrglt  28441  axcontlem7  28897  elntg2  28912  edglnl  29070  numedglnl  29071  ausgrumgri  29094  ausgrusgri  29095  usgrausgrb  29096  usgredg2vtxeuALT  29149  ushgredgedg  29156  ushgredgedgloop  29158  nbuhgr2vtx1edgb  29279  cusgrsize2inds  29381  upgrewlkle2  29534  wlkl1loop  29566  redwlk  29600  pthdivtx  29657  pthdadjvtx  29658  upgr2pthnlp  29662  upgrspthswlk  29668  clwlkl1loop  29713  cyclnumvtx  29730  wwlksnred  29822  wwlksnextbi  29824  elwwlks2ons3im  29884  umgrwwlks2on  29887  clwwlknwwlksn  29967  clwwlkinwwlk  29969  wwlksext2clwwlk  29986  1pthon2v  30082  uhgr3cyclex  30111  n4cyclfrgr  30220  frgrwopreg  30252  numclwwlk1lem2f1  30286  clwwlknonclwlknonf1o  30291  wlkl0  30296  frgrreggt1  30322  frgrreg  30323  frgrregord013  30324  chintcli  31260  spansnss  31500  elspansn4  31502  chscllem4  31569  hoadddir  31733  adjmul  32021  kbass6  32050  spansncv2  32222  sumdmdii  32344  nexple  32769  bnj1417  35031  lfuhgr2  35106  cusgredgex  35109  sat1el2xp  35366  fmlasuc  35373  satffunlem1lem1  35389  satffunlem2lem1  35391  mclsind  35557  iprodefisumlem  35727  btwndiff  36015  elicc3  36305  finminlem  36306  sdclem2  37736  clmgmOLD  37845  grpomndo  37869  zerdivemp1x  37941  lsmsat  39001  lsmcv2  39022  lcvat  39023  lsatcveq0  39025  lcvexchlem4  39030  lcvexchlem5  39031  islshpcv  39046  l1cvpat  39047  lshpkrlem6  39108  omlfh3N  39252  cvlsupr4  39338  cvlsupr5  39339  cvlsupr6  39340  2llnneN  39403  hlrelat3  39406  cvrval3  39407  cvrval4N  39408  cvrexchlem  39413  2atlt  39433  cvrat4  39437  atbtwnexOLDN  39441  atbtwnex  39442  athgt  39450  3dim1  39461  3dim2  39462  3dim3  39463  1cvratex  39467  llnle  39512  atcvrlln2  39513  atcvrlln  39514  2llnmat  39518  lplnle  39534  lplnnle2at  39535  lplnnlelln  39537  llncvrlpln2  39551  2llnjN  39561  lvoli2  39575  lvolnlelln  39578  lvolnlelpln  39579  4atlem10  39600  4atlem11  39603  4atlem12  39606  lplncvrlvol2  39609  2lplnj  39614  lneq2at  39772  lnatexN  39773  lnjatN  39774  lncvrat  39776  2lnat  39778  cdlemb  39788  paddasslem14  39827  llnexchb2  39863  dalawlem10  39874  dalawlem13  39877  dalawlem14  39878  dalaw  39880  pclclN  39885  pclfinN  39894  osumcllem11N  39960  lhp2lt  39995  lhpexle3lem  40005  4atexlem7  40069  ldilcnv  40109  ldilco  40110  ltrncnv  40140  trlval2  40157  cdleme24  40346  cdleme26ee  40354  cdleme28  40367  cdleme32le  40441  cdleme50trn2  40545  cdleme50ltrn  40551  cdleme  40554  cdlemf1  40555  cdlemf  40557  cdlemg1cex  40582  cdlemg2ce  40586  cdlemg18b  40673  ltrnco  40713  tendocan  40818  cdlemk28-3  40902  cdlemk11t  40940  dia2dimlem6  41063  dia2dimlem12  41069  dihlsscpre  41228  dihord4  41252  dihord5b  41253  dihmeetlem3N  41299  dihmeetlem20N  41320  dvh4dimlem  41437  lclkrlem2y  41525  mapdpglem24  41698  mapdpglem32  41699  mapdpg  41700  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  mapdh9a  41783  mapdh9aOLDN  41784  hdmap14lem6  41867  hdmapglem7  41923  indstrd  42181  nnadddir  42258  nnmulcom  42260  sn-addlid  42392  remulcand  42427  mzpexpmpt  42733  pellexlem5  42821  pellex  42823  pell14qrexpclnn0  42854  pellfundex  42874  monotuz  42930  monotoddzzfi  42931  rmxypos  42936  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.19lem3  42980  jm2.15nn0  42992  jm2.16nn0  42993  aomclem2  43044  aomclem6  43048  dfac11  43051  hbtlem5  43117  cnsrexpcl  43154  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  44199  3impexpbicomi  44471  ee333  44497  eel12131  44702  eel2122old  44707  e333  44722  ordelordALTVD  44856  refsumcn  45024  uzwo4  45047  ssinc  45081  ssdec  45082  iunincfi  45088  restuni3  45112  eliuniin2  45114  rabssd  45136  reximdd  45142  suprnmpt  45168  disjf1o  45185  disjinfi  45186  ssnnf1octb  45188  choicefi  45194  mapssbi  45207  unirnmapsn  45208  iunmapsn  45211  rnmptlb  45237  rnmptbddlem  45238  infnsuprnmpt  45244  fperiodmullem  45301  upbdrech  45303  ssfiunibd  45307  supxrgere  45329  iuneqfzuzlem  45330  supxrgelem  45333  supxrge  45334  suplesup  45335  infrpge  45347  infleinf  45368  suplesup2  45372  supxrunb3  45395  infleinf2  45410  rexabslelem  45414  infrnmptle  45419  infxrunb3rnmpt  45424  iccshift  45516  iooshift  45520  fmul01  45578  fmuldfeq  45581  fmul01lt1  45584  mullimc  45614  islptre  45617  mullimcf  45621  limcperiod  45626  islpcn  45637  limsupre  45639  limcleqr  45642  neglimc  45645  addlimc  45646  0ellimcdiv  45647  limclner  45649  fnlimfvre  45672  limsuppnflem  45708  limsupmnfuzlem  45724  limsupre3lem  45730  limsupre3uzlem  45733  climuzlem  45741  limsupgtlem  45775  coskpi2  45864  cosknegpi  45867  cncfshift  45872  cncfperiod  45877  icccncfext  45885  dvnmptdivc  45936  dvnmptconst  45939  dvnmul  45941  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  iblspltprt  45971  itgspltprt  45977  itgperiod  45979  ismbl3  45984  stoweidlem3  46001  stoweidlem31  46029  stoweidlem59  46057  stirlinglem13  46084  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem51  46155  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem80  46184  fourierdlem81  46185  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem97  46201  elaa2  46232  qndenserrnopnlem  46295  salexct  46332  subsaliuncl  46356  subsalsal  46357  sge0tsms  46378  sge0f1o  46380  sge0fsum  46385  sge0supre  46387  sge0sup  46389  sge0rnbnd  46391  sge0gerp  46393  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resrn  46402  sge0resplit  46404  sge0split  46407  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0rpcpnf  46419  sge0isum  46425  sge0xp  46427  sge0xaddlem2  46432  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  nnfoctbdjlem  46453  nnfoctbdj  46454  iundjiun  46458  meadjiunlem  46463  voliunsge0lem  46470  meaiuninclem  46478  meaiininc2  46486  carageniuncllem1  46519  carageniuncllem2  46520  caratheodorylem1  46524  caratheodorylem2  46525  isomenndlem  46528  ovnsupge0  46555  ovnlerp  46560  ovncvrrp  46562  ovnsubaddlem1  46568  hoidmvval0  46585  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem2  46600  opnvonmbllem2  46631  ovnovollem3  46656  vonioo  46680  vonicc  46683  pimiooltgt  46708  sssmf  46736  smfaddlem1  46761  smflimlem6  46774  smfmullem4  46792  smfpimbor1lem1  46796  smfco  46800  smfpimcc  46806  smflimmpt  46808  smfinflem  46815  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminfmpt  46830  cfsetsnfsetf1  47060  2tceilhalfelfzo1  47333  elsetpreimafveqfv  47393  iccpartiltu  47423  sprsymrelfvlem  47491  reuopreuprim  47527  goldbachth  47548  fmtnofac1  47571  prmdvdsfmtnof1lem1  47585  lighneal  47612  grimuhgr  47887  uhgrimedgi  47890  uhgrimisgrgriclem  47930  clnbgrgrim  47934  grimedg  47935  usgrgrtrirex  47949  isubgr3stgrlem3  47967  isubgr3stgrlem6  47970  uspgrlimlem2  47988  grlimgrtri  47995  grlicsym  48005  clnbgr3stgrgrlic  48011  gpgusgralem  48047  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  uspgropssxp  48132  rngccatidALTV  48260  ringccatidALTV  48294  lcosslsp  48427  fllog2  48557  dignn0flhalf  48607  fv1arycl  48626  1arymaptf1  48631  fv2arycl  48637  2arymaptf1  48642  itschlc0yqe  48749  itsclc0xyqsol  48757  seposep  48914  iscnrm3lem6  48926  iunord  49665  setrec2fun  49681