Theorem 3exp 1115

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 1114	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 422	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3expb  1116  3expib  1118  3com12  1119  3com13  1120  pm3.2an3  1336  3exp1  1348  3expd  1349  exp5o  1351  3ecase  1470  rexlimdv3a  3289  rabssdv  4054  reupick2  4292  disjiund  5059  otiunsndisj  5413  wefrc  5552  predpo  6169  tz7.7  6220  unizlim  6310  fvelimad  6735  fveqdmss  6849  f1oiso2  7108  ssorduni  7503  suceloni  7531  tfisi  7576  funeldmdif  7750  poxp  7825  smo11  8004  tfrlem5  8019  odi  8208  omass  8209  nndi  8252  nnmass  8253  undifixp  8501  findcard  8760  ac6sfi  8765  domunfican  8794  mapfien2  8875  fisup2g  8935  fiinf2g  8967  indcardi  9470  acndom  9480  ackbij1lem16  9660  infpssrlem4  9731  fin23lem11  9742  isfin2-2  9744  fin23lem34  9771  fin1a2lem10  9834  hsmexlem2  9852  axcc3  9863  domtriomlem  9867  axdc3lem2  9876  axdc3lem4  9878  axcclem  9882  ttukeyg  9942  axdclem2  9945  axacndlem4  10035  axacndlem5  10036  axacnd  10037  tskr1om2  10193  tskwe2  10198  tskord  10205  tskcard  10206  tskuni  10208  tskwun  10209  gruiin  10235  grudomon  10242  gruina  10243  mulcanpi  10325  adderpq  10381  mulerpq  10382  dedekindle  10807  divgt0  11511  divge0  11512  nnne0  11674  uzind  12077  uzind2  12078  iccsplit  12874  ssnn0fi  13356  expmordi  13534  sqlecan  13574  modexp  13602  expnngt1  13605  facavg  13664  2cshwcshw  14190  relexpcnv  14397  relexpreld  14402  relexpaddnn  14413  relexpaddg  14415  pwdif  15226  prodfn0  15253  prodfrec  15254  ntrivcvgfvn0  15258  fprodabs  15331  bpolycl  15409  bpolydif  15412  fprodefsum  15451  dvdsmodexp  15618  dvdsaddre2b  15660  dvdsnprmd  16037  2mulprm  16040  prmndvdsfaclt  16070  ncoprmlnprm  16071  fermltl  16124  pceu  16186  setsstruct2  16524  setsstruct  16526  mreexexd  16922  isglbd  17730  symgpssefmnd  18527  pmtrfrn  18589  psgnunilem4  18628  ablsimpgprmd  19240  mulgass2  19354  islss4  19737  lspsneu  19898  lspfixed  19903  lspexch  19904  lsmcv  19916  lspsolvlem  19917  xrsdsreclblem  20594  isphld  20801  mdetralt  21220  mdetunilem9  21232  fiinopn  21512  neips  21724  tpnei  21732  neindisj2  21734  opnneiid  21737  hausnei2  21964  cmpsublem  22010  cmpsub  22011  cmpcld  22013  comppfsc  22143  filufint  22531  cfinufil  22539  rnelfm  22564  alexsubALTlem1  22658  alexsubALTlem4  22661  alexsubALT  22662  tsmsxp  22766  neibl  23114  tngngp3  23268  tgqioo  23411  ovolunlem2  24102  iunmbl2  24161  itg1le  24317  vieta1  24904  aannenlem2  24921  aalioulem3  24926  aalioulem4  24927  aaliou2  24932  wilthlem3  25650  bcmono  25856  gausslemma2dlem1a  25944  iscgrglt  26303  axcontlem7  26759  elntg2  26774  edglnl  26931  numedglnl  26932  ausgrumgri  26955  ausgrusgri  26956  usgrausgrb  26957  usgredg2vtxeuALT  27007  ushgredgedg  27014  ushgredgedgloop  27016  nbuhgr2vtx1edgb  27137  cusgrsize2inds  27238  upgrewlkle2  27391  wlkl1loop  27422  redwlk  27457  pthdivtx  27513  pthdadjvtx  27514  upgr2pthnlp  27516  upgrspthswlk  27522  clwlkl1loop  27567  wwlksnred  27673  wwlksnextbi  27675  elwwlks2ons3im  27736  umgrwwlks2on  27739  clwwlknwwlksn  27819  clwwlkinwwlk  27821  wwlksext2clwwlk  27839  1pthon2v  27935  uhgr3cyclex  27964  n4cyclfrgr  28073  frgrwopreg  28105  numclwwlk1lem2f1  28139  clwwlknonclwlknonf1o  28144  wlkl0  28149  frgrreggt1  28175  frgrreg  28176  frgrregord013  28177  chintcli  29111  spansnss  29351  elspansn4  29353  chscllem4  29420  hoadddir  29584  adjmul  29872  kbass6  29901  spansncv2  30073  sumdmdii  30195  nexple  31272  bnj1417  32317  lfuhgr2  32369  cusgredgex  32372  sat1el2xp  32630  fmlasuc  32637  satffunlem1lem1  32653  satffunlem2lem1  32655  mclsind  32821  iprodefisumlem  32976  poseq  33099  fpr3g  33126  frrlem10  33136  btwndiff  33492  elicc3  33669  finminlem  33670  sdclem2  35021  clmgmOLD  35133  grpomndo  35157  zerdivemp1x  35229  lsmsat  36148  lsmcv2  36169  lcvat  36170  lsatcveq0  36172  lcvexchlem4  36177  lcvexchlem5  36178  islshpcv  36193  l1cvpat  36194  lshpkrlem6  36255  omlfh3N  36399  cvlsupr4  36485  cvlsupr5  36486  cvlsupr6  36487  2llnneN  36549  hlrelat3  36552  cvrval3  36553  cvrval4N  36554  cvrexchlem  36559  2atlt  36579  cvrat4  36583  atbtwnexOLDN  36587  atbtwnex  36588  athgt  36596  3dim1  36607  3dim2  36608  3dim3  36609  1cvratex  36613  llnle  36658  atcvrlln2  36659  atcvrlln  36660  2llnmat  36664  lplnle  36680  lplnnle2at  36681  lplnnlelln  36683  llncvrlpln2  36697  2llnjN  36707  lvoli2  36721  lvolnlelln  36724  lvolnlelpln  36725  4atlem10  36746  4atlem11  36749  4atlem12  36752  lplncvrlvol2  36755  2lplnj  36760  lneq2at  36918  lnatexN  36919  lnjatN  36920  lncvrat  36922  2lnat  36924  cdlemb  36934  paddasslem14  36973  llnexchb2  37009  dalawlem10  37020  dalawlem13  37023  dalawlem14  37024  dalaw  37026  pclclN  37031  pclfinN  37040  osumcllem11N  37106  lhp2lt  37141  lhpexle3lem  37151  4atexlem7  37215  ldilcnv  37255  ldilco  37256  ltrncnv  37286  trlval2  37303  cdleme24  37492  cdleme26ee  37500  cdleme28  37513  cdleme32le  37587  cdleme50trn2  37691  cdleme50ltrn  37697  cdleme  37700  cdlemf1  37701  cdlemf  37703  cdlemg1cex  37728  cdlemg2ce  37732  cdlemg18b  37819  ltrnco  37859  tendocan  37964  cdlemk28-3  38048  cdlemk11t  38086  dia2dimlem6  38209  dia2dimlem12  38215  dihlsscpre  38374  dihord4  38398  dihord5b  38399  dihmeetlem3N  38445  dihmeetlem20N  38466  dvh4dimlem  38583  lclkrlem2y  38671  mapdpglem24  38844  mapdpglem32  38845  mapdpg  38846  baerlem3lem2  38850  baerlem5alem2  38851  baerlem5blem2  38852  mapdh9a  38929  mapdh9aOLDN  38930  hdmap14lem6  39013  hdmapglem7  39069  nnadddir  39169  nnmulcom  39171  nn0rppwr  39188  sn-addid2  39240  remulcand  39256  mzpexpmpt  39348  pellexlem5  39436  pellex  39438  pell14qrexpclnn0  39469  pellfundex  39489  monotuz  39544  monotoddzzfi  39545  rmxypos  39550  jm2.17a  39563  jm2.17b  39564  rmygeid  39567  jm2.19lem3  39594  jm2.15nn0  39606  jm2.16nn0  39607  aomclem2  39661  aomclem6  39665  dfac11  39668  hbtlem5  39734  cnsrexpcl  39771  relexpxpnnidm  40054  relexpiidm  40055  relexpss1d  40056  iunrelexpmin1  40059  relexpmulnn  40060  iunrelexpmin2  40063  relexp01min  40064  relexp0a  40067  relexpxpmin  40068  relexpaddss  40069  trclimalb2  40077  tfindsd  40570  3impexpbicomi  40820  ee333  40847  eel12131  41053  eel2122old  41058  e333  41073  ordelordALTVD  41207  refsumcn  41293  uzwo4  41321  ssinc  41359  ssdec  41360  iunincfi  41366  restuni3  41390  eliuniin2  41392  rabssd  41417  reximdd  41427  suprnmpt  41436  disjf1o  41458  fompt  41459  disjinfi  41460  ssnnf1octb  41462  choicefi  41469  mapssbi  41482  unirnmapsn  41483  ssmapsn  41485  iunmapsn  41486  funimassd  41503  rnmptlb  41520  rnmptbddlem  41521  infnsuprnmpt  41528  fperiodmullem  41576  upbdrech  41578  ssfiunibd  41582  supxrgere  41607  iuneqfzuzlem  41608  supxrgelem  41611  supxrge  41612  suplesup  41613  infrpge  41625  infleinf  41646  suplesup2  41650  supxrunb3  41678  infleinf2  41694  rexabslelem  41698  infrnmptle  41703  infxrunb3rnmpt  41708  iccshift  41800  iooshift  41804  fmul01  41867  fmuldfeq  41870  fmul01lt1  41873  mullimc  41903  islptre  41906  mullimcf  41910  limcperiod  41915  islpcn  41926  limsupre  41928  limcleqr  41931  neglimc  41934  addlimc  41935  0ellimcdiv  41936  limclner  41938  fnlimfvre  41961  limsuppnflem  41997  limsupmnfuzlem  42013  limsupre3lem  42019  limsupre3uzlem  42022  climuzlem  42030  limsupgtlem  42064  coskpi2  42153  cosknegpi  42156  cncfshift  42163  cncfperiod  42168  icccncfext  42176  dvnmptdivc  42229  dvnmptconst  42232  dvnmul  42234  dvmptfprodlem  42235  dvmptfprod  42236  dvnprodlem1  42237  dvnprodlem2  42238  iblspltprt  42264  itgspltprt  42270  itgperiod  42272  ismbl3  42278  stoweidlem3  42295  stoweidlem31  42323  stoweidlem59  42351  stirlinglem13  42378  fourierdlem41  42440  fourierdlem42  42441  fourierdlem48  42446  fourierdlem51  42449  fourierdlem53  42451  fourierdlem70  42468  fourierdlem71  42469  fourierdlem73  42471  fourierdlem80  42478  fourierdlem81  42479  fourierdlem89  42487  fourierdlem91  42489  fourierdlem93  42491  fourierdlem97  42495  elaa2  42526  qndenserrnopnlem  42589  salexct  42624  subsaliuncl  42648  subsalsal  42649  sge0tsms  42669  sge0f1o  42671  sge0fsum  42676  sge0supre  42678  sge0sup  42680  sge0rnbnd  42682  sge0gerp  42684  sge0pnffigt  42685  sge0lefi  42687  sge0ltfirp  42689  sge0resrn  42693  sge0resplit  42695  sge0split  42698  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0iunmpt  42707  sge0rpcpnf  42710  sge0isum  42716  sge0xp  42718  sge0xaddlem2  42723  sge0uzfsumgt  42733  sge0seq  42735  sge0reuz  42736  nnfoctbdjlem  42744  nnfoctbdj  42745  iundjiun  42749  meadjiunlem  42754  voliunsge0lem  42761  meaiuninclem  42769  meaiininc2  42777  carageniuncllem1  42810  carageniuncllem2  42811  caratheodorylem1  42815  caratheodorylem2  42816  isomenndlem  42819  ovnsupge0  42846  ovnlerp  42851  ovncvrrp  42853  ovnsubaddlem1  42859  hoidmvval0  42876  hoidmv1lelem3  42882  hoidmv1le  42883  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem2  42891  opnvonmbllem2  42922  ovolval5lem3  42943  ovnovollem3  42947  vonioo  42971  vonicc  42974  pimiooltgt  42996  sssmf  43022  smfaddlem1  43046  smflimlem6  43059  smfmullem4  43076  smfpimbor1lem1  43080  smfco  43084  smfpimcc  43089  smflimmpt  43091  smfinflem  43098  smflimsuplem7  43107  smflimsuplem8  43108  smflimsupmpt  43110  smfliminfmpt  43113  elsetpreimafveqfv  43559  iccpartiltu  43589  sprsymrelfvlem  43659  reuopreuprim  43695  goldbachth  43716  fmtnofac1  43739  prmdvdsfmtnof1lem1  43753  lighneal  43783  isomgrsym  44008  isomgrtr  44011  uspgropssxp  44026  rngccatidALTV  44267  ringccatidALTV  44330  nzerooringczr  44350  lcosslsp  44500  fllog2  44635  dignn0flhalf  44685  itschlc0yqe  44754  itsclc0xyqsol  44762  iunord  44786  setrec2fun  44802