Theorem 3exp 1117

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3expb  1118  3expib  1120  3com12  1121  3com13  1122  pm3.2an3  1338  3exp1  1350  3expd  1351  exp5o  1353  3ecase  1472  rexlimdv3a  3213  rabssdv  4009  reupick2  4256  disjiund  5065  otiunsndisj  5433  wefrc  5579  tz7.7  6282  unizlim  6373  fvelimad  6823  fveqdmss  6943  f1oiso2  7208  ssorduni  7611  suceloni  7640  tfisi  7685  funeldmdif  7867  poxp  7945  fpr3g  8077  frrlem10  8087  smo11  8171  tfrlem5  8187  odi  8377  omass  8378  nndi  8421  nnmass  8422  undifixp  8685  findcard  8900  ac6sfi  9004  domunfican  9033  mapfien2  9114  fisup2g  9173  fiinf2g  9205  indcardi  9744  acndom  9754  ackbij1lem16  9938  infpssrlem4  10009  fin23lem11  10020  isfin2-2  10022  fin23lem34  10049  fin1a2lem10  10112  hsmexlem2  10130  axcc3  10141  domtriomlem  10145  axdc3lem2  10154  axdc3lem4  10156  axcclem  10160  ttukeyg  10220  axdclem2  10223  axacndlem4  10313  axacndlem5  10314  axacnd  10315  tskr1om2  10471  tskwe2  10476  tskord  10483  tskcard  10484  tskuni  10486  tskwun  10487  gruiin  10513  grudomon  10520  gruina  10521  mulcanpi  10603  adderpq  10659  mulerpq  10660  dedekindle  11085  divgt0  11789  divge0  11790  nnne0  11953  uzind  12358  uzind2  12359  iccsplit  13162  ssnn0fi  13649  expmordi  13829  sqlecan  13869  modexp  13897  expnngt1  13900  facavg  13959  2cshwcshw  14482  relexpcnv  14690  relexpaddnn  14706  relexpaddg  14708  pwdif  15524  prodfn0  15550  prodfrec  15551  ntrivcvgfvn0  15555  fprodabs  15628  bpolycl  15706  bpolydif  15709  fprodefsum  15748  dvdsmodexp  15915  dvdsaddre2b  15960  dvdsnprmd  16339  2mulprm  16342  prmndvdsfaclt  16374  ncoprmlnprm  16376  fermltl  16429  pceu  16491  setsstruct2  16819  setsstruct  16821  mreexexd  17301  isglbd  18171  symgpssefmnd  18947  pmtrfrn  19010  psgnunilem4  19049  ablsimpgprmd  19662  mulgass2  19784  islss4  20168  lspsneu  20329  lspfixed  20334  lspexch  20335  lsmcv  20347  lspsolvlem  20348  xrsdsreclblem  20588  isphld  20803  mdetralt  21701  mdetunilem9  21713  fiinopn  21994  neips  22208  tpnei  22216  neindisj2  22218  opnneiid  22221  hausnei2  22448  cmpsublem  22494  cmpsub  22495  cmpcld  22497  comppfsc  22627  filufint  23015  cfinufil  23023  rnelfm  23048  alexsubALTlem1  23142  alexsubALTlem4  23145  alexsubALT  23146  tsmsxp  23250  neibl  23601  tngngp3  23764  tgqioo  23907  ovolunlem2  24605  iunmbl2  24664  itg1le  24821  vieta1  25415  aannenlem2  25432  aalioulem3  25437  aalioulem4  25438  aaliou2  25443  wilthlem3  26162  bcmono  26368  gausslemma2dlem1a  26456  iscgrglt  26818  axcontlem7  27281  elntg2  27296  edglnl  27456  numedglnl  27457  ausgrumgri  27480  ausgrusgri  27481  usgrausgrb  27482  usgredg2vtxeuALT  27532  ushgredgedg  27539  ushgredgedgloop  27541  nbuhgr2vtx1edgb  27662  cusgrsize2inds  27763  upgrewlkle2  27916  wlkl1loop  27947  redwlk  27982  pthdivtx  28038  pthdadjvtx  28039  upgr2pthnlp  28041  upgrspthswlk  28047  clwlkl1loop  28092  wwlksnred  28198  wwlksnextbi  28200  elwwlks2ons3im  28260  umgrwwlks2on  28263  clwwlknwwlksn  28343  clwwlkinwwlk  28345  wwlksext2clwwlk  28362  1pthon2v  28458  uhgr3cyclex  28487  n4cyclfrgr  28596  frgrwopreg  28628  numclwwlk1lem2f1  28662  clwwlknonclwlknonf1o  28667  wlkl0  28672  frgrreggt1  28698  frgrreg  28699  frgrregord013  28700  chintcli  29634  spansnss  29874  elspansn4  29876  chscllem4  29943  hoadddir  30107  adjmul  30395  kbass6  30424  spansncv2  30596  sumdmdii  30718  nexple  31919  bnj1417  32963  lfuhgr2  33022  cusgredgex  33025  sat1el2xp  33283  fmlasuc  33290  satffunlem1lem1  33306  satffunlem2lem1  33308  mclsind  33474  iprodefisumlem  33654  ttrclss  33748  ttrclselem2  33754  poseq  33771  sslttr  33970  ssltun1  33971  ssltun2  33972  sltlpss  34056  btwndiff  34298  elicc3  34475  finminlem  34476  sdclem2  35869  clmgmOLD  35978  grpomndo  36002  zerdivemp1x  36074  lsmsat  36991  lsmcv2  37012  lcvat  37013  lsatcveq0  37015  lcvexchlem4  37020  lcvexchlem5  37021  islshpcv  37036  l1cvpat  37037  lshpkrlem6  37098  omlfh3N  37242  cvlsupr4  37328  cvlsupr5  37329  cvlsupr6  37330  2llnneN  37392  hlrelat3  37395  cvrval3  37396  cvrval4N  37397  cvrexchlem  37402  2atlt  37422  cvrat4  37426  atbtwnexOLDN  37430  atbtwnex  37431  athgt  37439  3dim1  37450  3dim2  37451  3dim3  37452  1cvratex  37456  llnle  37501  atcvrlln2  37502  atcvrlln  37503  2llnmat  37507  lplnle  37523  lplnnle2at  37524  lplnnlelln  37526  llncvrlpln2  37540  2llnjN  37550  lvoli2  37564  lvolnlelln  37567  lvolnlelpln  37568  4atlem10  37589  4atlem11  37592  4atlem12  37595  lplncvrlvol2  37598  2lplnj  37603  lneq2at  37761  lnatexN  37762  lnjatN  37763  lncvrat  37765  2lnat  37767  cdlemb  37777  paddasslem14  37816  llnexchb2  37852  dalawlem10  37863  dalawlem13  37866  dalawlem14  37867  dalaw  37869  pclclN  37874  pclfinN  37883  osumcllem11N  37949  lhp2lt  37984  lhpexle3lem  37994  4atexlem7  38058  ldilcnv  38098  ldilco  38099  ltrncnv  38129  trlval2  38146  cdleme24  38335  cdleme26ee  38343  cdleme28  38356  cdleme32le  38430  cdleme50trn2  38534  cdleme50ltrn  38540  cdleme  38543  cdlemf1  38544  cdlemf  38546  cdlemg1cex  38571  cdlemg2ce  38575  cdlemg18b  38662  ltrnco  38702  tendocan  38807  cdlemk28-3  38891  cdlemk11t  38929  dia2dimlem6  39052  dia2dimlem12  39058  dihlsscpre  39217  dihord4  39241  dihord5b  39242  dihmeetlem3N  39288  dihmeetlem20N  39309  dvh4dimlem  39426  lclkrlem2y  39514  mapdpglem24  39687  mapdpglem32  39688  mapdpg  39689  baerlem3lem2  39693  baerlem5alem2  39694  baerlem5blem2  39695  mapdh9a  39772  mapdh9aOLDN  39773  hdmap14lem6  39856  hdmapglem7  39912  nnadddir  40263  nnmulcom  40265  nn0rppwr  40296  sn-addid2  40350  remulcand  40383  mzpexpmpt  40525  pellexlem5  40613  pellex  40615  pell14qrexpclnn0  40646  pellfundex  40666  monotuz  40721  monotoddzzfi  40722  rmxypos  40727  jm2.17a  40740  jm2.17b  40741  rmygeid  40744  jm2.19lem3  40771  jm2.15nn0  40783  jm2.16nn0  40784  aomclem2  40838  aomclem6  40842  dfac11  40845  hbtlem5  40911  cnsrexpcl  40948  relexpxpnnidm  41242  relexpiidm  41243  relexpss1d  41244  iunrelexpmin1  41247  relexpmulnn  41248  iunrelexpmin2  41251  relexp01min  41252  relexp0a  41255  relexpxpmin  41256  relexpaddss  41257  trclimalb2  41265  tfindsd  41754  3impexpbicomi  42031  ee333  42058  eel12131  42264  eel2122old  42269  e333  42284  ordelordALTVD  42418  refsumcn  42504  uzwo4  42532  ssinc  42568  ssdec  42569  iunincfi  42575  restuni3  42598  eliuniin2  42600  rabssd  42622  reximdd  42632  suprnmpt  42641  disjf1o  42660  fompt  42661  disjinfi  42662  ssnnf1octb  42664  choicefi  42671  mapssbi  42684  unirnmapsn  42685  ssmapsn  42687  iunmapsn  42688  funimassd  42701  rnmptlb  42719  rnmptbddlem  42720  infnsuprnmpt  42727  fperiodmullem  42774  upbdrech  42776  ssfiunibd  42780  supxrgere  42804  iuneqfzuzlem  42805  supxrgelem  42808  supxrge  42809  suplesup  42810  infrpge  42822  infleinf  42843  suplesup2  42847  supxrunb3  42871  infleinf2  42886  rexabslelem  42890  infrnmptle  42895  infxrunb3rnmpt  42900  iccshift  42988  iooshift  42992  fmul01  43053  fmuldfeq  43056  fmul01lt1  43059  mullimc  43089  islptre  43092  mullimcf  43096  limcperiod  43101  islpcn  43112  limsupre  43114  limcleqr  43117  neglimc  43120  addlimc  43121  0ellimcdiv  43122  limclner  43124  fnlimfvre  43147  limsuppnflem  43183  limsupmnfuzlem  43199  limsupre3lem  43205  limsupre3uzlem  43208  climuzlem  43216  limsupgtlem  43250  coskpi2  43339  cosknegpi  43342  cncfshift  43347  cncfperiod  43352  icccncfext  43360  dvnmptdivc  43411  dvnmptconst  43414  dvnmul  43416  dvmptfprodlem  43417  dvmptfprod  43418  dvnprodlem1  43419  dvnprodlem2  43420  iblspltprt  43446  itgspltprt  43452  itgperiod  43454  ismbl3  43459  stoweidlem3  43476  stoweidlem31  43504  stoweidlem59  43532  stirlinglem13  43559  fourierdlem41  43621  fourierdlem42  43622  fourierdlem48  43627  fourierdlem51  43630  fourierdlem70  43649  fourierdlem71  43650  fourierdlem73  43652  fourierdlem80  43659  fourierdlem81  43660  fourierdlem89  43668  fourierdlem91  43670  fourierdlem93  43672  fourierdlem97  43676  elaa2  43707  qndenserrnopnlem  43770  salexct  43805  subsaliuncl  43829  subsalsal  43830  sge0tsms  43850  sge0f1o  43852  sge0fsum  43857  sge0supre  43859  sge0sup  43861  sge0rnbnd  43863  sge0gerp  43865  sge0pnffigt  43866  sge0lefi  43868  sge0ltfirp  43870  sge0resrn  43874  sge0resplit  43876  sge0split  43879  sge0iunmptlemfi  43883  sge0iunmptlemre  43885  sge0iunmpt  43888  sge0rpcpnf  43891  sge0isum  43897  sge0xp  43899  sge0xaddlem2  43904  sge0uzfsumgt  43914  sge0seq  43916  sge0reuz  43917  nnfoctbdjlem  43925  nnfoctbdj  43926  iundjiun  43930  meadjiunlem  43935  voliunsge0lem  43942  meaiuninclem  43950  meaiininc2  43958  carageniuncllem1  43991  carageniuncllem2  43992  caratheodorylem1  43996  caratheodorylem2  43997  isomenndlem  44000  ovnsupge0  44027  ovnlerp  44032  ovncvrrp  44034  ovnsubaddlem1  44040  hoidmvval0  44057  hoidmv1lelem3  44063  hoidmv1le  44064  hoidmvlelem1  44065  hoidmvlelem2  44066  hoidmvlelem3  44067  ovnhoilem2  44072  opnvonmbllem2  44103  ovolval5lem3  44124  ovnovollem3  44128  vonioo  44152  vonicc  44155  pimiooltgt  44177  sssmf  44203  smfaddlem1  44227  smflimlem6  44240  smfmullem4  44257  smfpimbor1lem1  44261  smfco  44265  smfpimcc  44270  smflimmpt  44272  smfinflem  44279  smflimsuplem7  44288  smflimsuplem8  44289  smflimsupmpt  44291  smfliminfmpt  44294  cfsetsnfsetf1  44482  elsetpreimafveqfv  44774  iccpartiltu  44804  sprsymrelfvlem  44872  reuopreuprim  44908  goldbachth  44929  fmtnofac1  44952  prmdvdsfmtnof1lem1  44966  lighneal  44993  isomgrsym  45218  isomgrtr  45221  uspgropssxp  45236  rngccatidALTV  45477  ringccatidALTV  45540  nzerooringczr  45560  lcosslsp  45709  fllog2  45844  dignn0flhalf  45894  fv1arycl  45913  1arymaptf1  45918  fv2arycl  45924  2arymaptf1  45929  itschlc0yqe  46036  itsclc0xyqsol  46044  seposep  46149  iscnrm3lem6  46162  iunord  46312  setrec2fun  46328