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  3137  rabssdv  4020  reupick2  4276  disjiund  5077  otiunsndisj  5455  wefrc  5605  tz7.7  6327  unizlim  6425  funimassd  6883  fvelimad  6884  fveqdmss  7006  fompt  7046  f1oiso2  7281  ssorduni  7707  tfisi  7784  resf1extb  7859  funeldmdif  7975  poxp  8053  poseq  8083  fpr3g  8210  frrlem10  8220  smo11  8279  tfrlem5  8294  odi  8489  omass  8490  nndi  8533  nnmass  8534  naddoa  8612  undifixp  8853  findcard  9068  php3  9113  ac6sfi  9163  domunfican  9201  mapfien2  9288  fisup2g  9348  fiinf2g  9381  ttrclss  9605  ttrclselem2  9611  indcardi  9927  acndom  9937  ackbij1lem16  10120  infpssrlem4  10192  fin23lem11  10203  isfin2-2  10205  fin23lem34  10232  fin1a2lem10  10295  hsmexlem2  10313  axcc3  10324  domtriomlem  10328  axdc3lem2  10337  axdc3lem4  10339  axcclem  10343  ttukeyg  10403  axdclem2  10406  axacndlem4  10496  axacndlem5  10497  axacnd  10498  tskr1om2  10654  tskwe2  10659  tskord  10666  tskcard  10667  tskuni  10669  tskwun  10670  gruiin  10696  grudomon  10703  gruina  10704  mulcanpi  10786  adderpq  10842  mulerpq  10843  dedekindle  11272  divgt0  11985  divge0  11986  nnne0  12154  uzind  12560  uzind2  12561  iccsplit  13380  ssnn0fi  13887  expmordi  14069  sqlecan  14111  modexp  14140  expnngt1  14143  facavg  14203  2cshwcshw  14727  relexpcnv  14937  relexpaddnn  14953  relexpaddg  14955  pwdif  15770  prodfn0  15796  prodfrec  15797  ntrivcvgfvn0  15801  fprodabs  15876  bpolycl  15954  bpolydif  15957  fprodefsum  15997  dvdsmodexp  16166  dvdsaddre2b  16213  nn0rppwr  16467  dvdsnprmd  16596  2mulprm  16599  prmndvdsfaclt  16631  ncoprmlnprm  16634  fermltl  16690  pceu  16753  setsstruct2  17080  setsstruct  17082  mreexexd  17549  isglbd  18410  symgpssefmnd  19303  pmtrfrn  19365  psgnunilem4  19404  ablsimpgprmd  20024  mulgass2  20222  islss4  20890  lspsneu  21055  lspfixed  21060  lspexch  21061  lsmcv  21073  lspsolvlem  21074  rnglidlmcl  21148  xrsdsreclblem  21344  nzerooringczr  21412  isphld  21586  mdetralt  22518  mdetunilem9  22530  fiinopn  22811  neips  23023  tpnei  23031  neindisj2  23033  opnneiid  23036  hausnei2  23263  cmpsublem  23309  cmpsub  23310  cmpcld  23312  comppfsc  23442  filufint  23830  cfinufil  23838  rnelfm  23863  alexsubALTlem1  23957  alexsubALTlem4  23960  alexsubALT  23961  tsmsxp  24065  neibl  24411  tngngp3  24566  tgqioo  24710  ovolunlem2  25421  iunmbl2  25480  itg1le  25636  vieta1  26242  aannenlem2  26259  aalioulem3  26264  aalioulem4  26265  aaliou2  26270  wilthlem3  27002  bcmono  27210  gausslemma2dlem1a  27298  sslttr  27743  ssltun1  27744  ssltun2  27745  sltlpss  27848  precsexlem8  28147  precsexlem9  28148  precsex  28151  onsfi  28278  expscllem  28348  expsgt0  28355  pw2cut  28375  pw2cut2  28377  iscgrglt  28487  axcontlem7  28943  elntg2  28958  edglnl  29116  numedglnl  29117  ausgrumgri  29140  ausgrusgri  29141  usgrausgrb  29142  usgredg2vtxeuALT  29195  ushgredgedg  29202  ushgredgedgloop  29204  nbuhgr2vtx1edgb  29325  cusgrsize2inds  29427  upgrewlkle2  29580  wlkl1loop  29611  redwlk  29644  pthdivtx  29700  pthdadjvtx  29701  upgr2pthnlp  29705  upgrspthswlk  29711  clwlkl1loop  29756  cyclnumvtx  29773  wwlksnred  29865  wwlksnextbi  29867  elwwlks2ons3im  29927  umgrwwlks2on  29930  clwwlknwwlksn  30010  clwwlkinwwlk  30012  wwlksext2clwwlk  30029  1pthon2v  30125  uhgr3cyclex  30154  n4cyclfrgr  30263  frgrwopreg  30295  numclwwlk1lem2f1  30329  clwwlknonclwlknonf1o  30334  wlkl0  30339  frgrreggt1  30365  frgrreg  30366  frgrregord013  30367  chintcli  31303  spansnss  31543  elspansn4  31545  chscllem4  31612  hoadddir  31776  adjmul  32064  kbass6  32093  spansncv2  32265  sumdmdii  32387  nexple  32819  bnj1417  35045  lfuhgr2  35155  cusgredgex  35158  sat1el2xp  35415  fmlasuc  35422  satffunlem1lem1  35438  satffunlem2lem1  35440  mclsind  35606  iprodefisumlem  35776  btwndiff  36061  elicc3  36351  finminlem  36352  sdclem2  37782  clmgmOLD  37891  grpomndo  37915  zerdivemp1x  37987  lsmsat  39047  lsmcv2  39068  lcvat  39069  lsatcveq0  39071  lcvexchlem4  39076  lcvexchlem5  39077  islshpcv  39092  l1cvpat  39093  lshpkrlem6  39154  omlfh3N  39298  cvlsupr4  39384  cvlsupr5  39385  cvlsupr6  39386  2llnneN  39448  hlrelat3  39451  cvrval3  39452  cvrval4N  39453  cvrexchlem  39458  2atlt  39478  cvrat4  39482  atbtwnexOLDN  39486  atbtwnex  39487  athgt  39495  3dim1  39506  3dim2  39507  3dim3  39508  1cvratex  39512  llnle  39557  atcvrlln2  39558  atcvrlln  39559  2llnmat  39563  lplnle  39579  lplnnle2at  39580  lplnnlelln  39582  llncvrlpln2  39596  2llnjN  39606  lvoli2  39620  lvolnlelln  39623  lvolnlelpln  39624  4atlem10  39645  4atlem11  39648  4atlem12  39651  lplncvrlvol2  39654  2lplnj  39659  lneq2at  39817  lnatexN  39818  lnjatN  39819  lncvrat  39821  2lnat  39823  cdlemb  39833  paddasslem14  39872  llnexchb2  39908  dalawlem10  39919  dalawlem13  39922  dalawlem14  39923  dalaw  39925  pclclN  39930  pclfinN  39939  osumcllem11N  40005  lhp2lt  40040  lhpexle3lem  40050  4atexlem7  40114  ldilcnv  40154  ldilco  40155  ltrncnv  40185  trlval2  40202  cdleme24  40391  cdleme26ee  40399  cdleme28  40412  cdleme32le  40486  cdleme50trn2  40590  cdleme50ltrn  40596  cdleme  40599  cdlemf1  40600  cdlemf  40602  cdlemg1cex  40627  cdlemg2ce  40631  cdlemg18b  40718  ltrnco  40758  tendocan  40863  cdlemk28-3  40947  cdlemk11t  40985  dia2dimlem6  41108  dia2dimlem12  41114  dihlsscpre  41273  dihord4  41297  dihord5b  41298  dihmeetlem3N  41344  dihmeetlem20N  41365  dvh4dimlem  41482  lclkrlem2y  41570  mapdpglem24  41743  mapdpglem32  41744  mapdpg  41745  baerlem3lem2  41749  baerlem5alem2  41750  baerlem5blem2  41751  mapdh9a  41828  mapdh9aOLDN  41829  hdmap14lem6  41912  hdmapglem7  41968  indstrd  42226  nnadddir  42303  nnmulcom  42305  sn-addlid  42437  remulcand  42472  mzpexpmpt  42778  pellexlem5  42866  pellex  42868  pell14qrexpclnn0  42899  pellfundex  42919  monotuz  42974  monotoddzzfi  42975  rmxypos  42980  jm2.17a  42993  jm2.17b  42994  rmygeid  42997  jm2.19lem3  43024  jm2.15nn0  43036  jm2.16nn0  43037  aomclem2  43088  aomclem6  43092  dfac11  43095  hbtlem5  43161  cnsrexpcl  43198  cantnf2  43358  dflim5  43362  relexpxpnnidm  43736  relexpiidm  43737  relexpss1d  43738  iunrelexpmin1  43741  relexpmulnn  43742  iunrelexpmin2  43745  relexp01min  43746  relexp0a  43749  relexpxpmin  43750  relexpaddss  43751  trclimalb2  43759  tfindsd  44243  3impexpbicomi  44514  ee333  44540  eel12131  44745  eel2122old  44750  e333  44765  ordelordALTVD  44899  refsumcn  45067  uzwo4  45090  ssinc  45124  ssdec  45125  iunincfi  45131  restuni3  45155  eliuniin2  45157  rabssd  45179  reximdd  45185  suprnmpt  45211  disjf1o  45228  disjinfi  45229  ssnnf1octb  45231  choicefi  45237  mapssbi  45250  unirnmapsn  45251  iunmapsn  45254  rnmptlb  45280  rnmptbddlem  45281  infnsuprnmpt  45287  fperiodmullem  45344  upbdrech  45346  ssfiunibd  45350  supxrgere  45372  iuneqfzuzlem  45373  supxrgelem  45376  supxrge  45377  suplesup  45378  infrpge  45390  infleinf  45410  suplesup2  45414  supxrunb3  45437  infleinf2  45452  rexabslelem  45456  infrnmptle  45461  infxrunb3rnmpt  45466  iccshift  45558  iooshift  45562  fmul01  45620  fmuldfeq  45623  fmul01lt1  45626  mullimc  45656  islptre  45659  mullimcf  45663  limcperiod  45668  islpcn  45677  limsupre  45679  limcleqr  45682  neglimc  45685  addlimc  45686  0ellimcdiv  45687  limclner  45689  fnlimfvre  45712  limsuppnflem  45748  limsupmnfuzlem  45764  limsupre3lem  45770  limsupre3uzlem  45773  climuzlem  45781  limsupgtlem  45815  coskpi2  45904  cosknegpi  45907  cncfshift  45912  cncfperiod  45917  icccncfext  45925  dvnmptdivc  45976  dvnmptconst  45979  dvnmul  45981  dvmptfprodlem  45982  dvmptfprod  45983  dvnprodlem1  45984  dvnprodlem2  45985  iblspltprt  46011  itgspltprt  46017  itgperiod  46019  ismbl3  46024  stoweidlem3  46041  stoweidlem31  46069  stoweidlem59  46097  stirlinglem13  46124  fourierdlem41  46186  fourierdlem42  46187  fourierdlem48  46192  fourierdlem51  46195  fourierdlem70  46214  fourierdlem71  46215  fourierdlem73  46217  fourierdlem80  46224  fourierdlem81  46225  fourierdlem89  46233  fourierdlem91  46235  fourierdlem93  46237  fourierdlem97  46241  elaa2  46272  qndenserrnopnlem  46335  salexct  46372  subsaliuncl  46396  subsalsal  46397  sge0tsms  46418  sge0f1o  46420  sge0fsum  46425  sge0supre  46427  sge0sup  46429  sge0rnbnd  46431  sge0gerp  46433  sge0pnffigt  46434  sge0lefi  46436  sge0ltfirp  46438  sge0resrn  46442  sge0resplit  46444  sge0split  46447  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  sge0iunmpt  46456  sge0rpcpnf  46459  sge0isum  46465  sge0xp  46467  sge0xaddlem2  46472  sge0uzfsumgt  46482  sge0seq  46484  sge0reuz  46485  nnfoctbdjlem  46493  nnfoctbdj  46494  iundjiun  46498  meadjiunlem  46503  voliunsge0lem  46510  meaiuninclem  46518  meaiininc2  46526  carageniuncllem1  46559  carageniuncllem2  46560  caratheodorylem1  46564  caratheodorylem2  46565  isomenndlem  46568  ovnsupge0  46595  ovnlerp  46600  ovncvrrp  46602  ovnsubaddlem1  46608  hoidmvval0  46625  hoidmv1lelem3  46631  hoidmv1le  46632  hoidmvlelem1  46633  hoidmvlelem2  46634  hoidmvlelem3  46635  ovnhoilem2  46640  opnvonmbllem2  46671  ovnovollem3  46696  vonioo  46720  vonicc  46723  pimiooltgt  46748  sssmf  46776  smfaddlem1  46801  smflimlem6  46814  smfmullem4  46832  smfpimbor1lem1  46836  smfco  46840  smfpimcc  46846  smflimmpt  46848  smfinflem  46855  smflimsuplem7  46864  smflimsuplem8  46865  smflimsupmpt  46867  smfliminfmpt  46870  cfsetsnfsetf1  47090  2tceilhalfelfzo1  47363  elsetpreimafveqfv  47423  iccpartiltu  47453  sprsymrelfvlem  47521  reuopreuprim  47557  goldbachth  47578  fmtnofac1  47601  prmdvdsfmtnof1lem1  47615  lighneal  47642  grimuhgr  47918  uhgrimedgi  47921  uhgrimisgrgriclem  47961  clnbgrgrim  47965  grimedg  47966  usgrgrtrirex  47981  isubgr3stgrlem3  47999  isubgr3stgrlem6  48002  uspgrlimlem2  48020  grlimgrtri  48034  grlicsym  48044  clnbgr3stgrgrlic  48051  gpgusgralem  48087  gpgedgvtx1  48093  gpgvtxedg0  48094  gpgvtxedg1  48095  uspgropssxp  48175  rngccatidALTV  48303  ringccatidALTV  48337  lcosslsp  48470  fllog2  48600  dignn0flhalf  48650  fv1arycl  48669  1arymaptf1  48674  fv2arycl  48680  2arymaptf1  48685  itschlc0yqe  48792  itsclc0xyqsol  48800  seposep  48957  iscnrm3lem6  48969  iunord  49708  setrec2fun  49724