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 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  1120  3expib  1122  3com12  1123  3com13  1124  pm3.2an3  1340  3exp1  1352  3expd  1353  exp5o  1355  3ecase  1474  rexlimdv3a  3165  rabssdv  4098  reupick2  4350  disjiund  5157  otiunsndisj  5539  wefrc  5694  tz7.7  6421  unizlim  6518  funimassd  6988  fvelimad  6989  fveqdmss  7112  fompt  7152  f1oiso2  7388  ssorduni  7814  sucexeloniOLD  7846  suceloniOLD  7848  tfisi  7896  funeldmdif  8089  poxp  8169  poseq  8199  fpr3g  8326  frrlem10  8336  smo11  8420  tfrlem5  8436  odi  8635  omass  8636  nndi  8679  nnmass  8680  naddoa  8758  undifixp  8992  findcard  9229  php3  9275  ac6sfi  9348  domunfican  9389  mapfien2  9478  fisup2g  9537  fiinf2g  9569  ttrclss  9789  ttrclselem2  9795  indcardi  10110  acndom  10120  ackbij1lem16  10303  infpssrlem4  10375  fin23lem11  10386  isfin2-2  10388  fin23lem34  10415  fin1a2lem10  10478  hsmexlem2  10496  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axcclem  10526  ttukeyg  10586  axdclem2  10589  axacndlem4  10679  axacndlem5  10680  axacnd  10681  tskr1om2  10837  tskwe2  10842  tskord  10849  tskcard  10850  tskuni  10852  tskwun  10853  gruiin  10879  grudomon  10886  gruina  10887  mulcanpi  10969  adderpq  11025  mulerpq  11026  dedekindle  11454  divgt0  12163  divge0  12164  nnne0  12327  uzind  12735  uzind2  12736  iccsplit  13545  ssnn0fi  14036  expmordi  14217  sqlecan  14258  modexp  14287  expnngt1  14290  facavg  14350  2cshwcshw  14874  relexpcnv  15084  relexpaddnn  15100  relexpaddg  15102  pwdif  15916  prodfn0  15942  prodfrec  15943  ntrivcvgfvn0  15947  fprodabs  16022  bpolycl  16100  bpolydif  16103  fprodefsum  16143  dvdsmodexp  16310  dvdsaddre2b  16355  nn0rppwr  16608  dvdsnprmd  16737  2mulprm  16740  prmndvdsfaclt  16772  ncoprmlnprm  16775  fermltl  16831  pceu  16893  setsstruct2  17221  setsstruct  17223  mreexexd  17706  isglbd  18579  symgpssefmnd  19437  pmtrfrn  19500  psgnunilem4  19539  ablsimpgprmd  20159  mulgass2  20332  islss4  20983  lspsneu  21148  lspfixed  21153  lspexch  21154  lsmcv  21166  lspsolvlem  21167  rnglidlmcl  21249  xrsdsreclblem  21453  nzerooringczr  21514  isphld  21695  mdetralt  22635  mdetunilem9  22647  fiinopn  22928  neips  23142  tpnei  23150  neindisj2  23152  opnneiid  23155  hausnei2  23382  cmpsublem  23428  cmpsub  23429  cmpcld  23431  comppfsc  23561  filufint  23949  cfinufil  23957  rnelfm  23982  alexsubALTlem1  24076  alexsubALTlem4  24079  alexsubALT  24080  tsmsxp  24184  neibl  24535  tngngp3  24698  tgqioo  24841  ovolunlem2  25552  iunmbl2  25611  itg1le  25768  vieta1  26372  aannenlem2  26389  aalioulem3  26394  aalioulem4  26395  aaliou2  26400  wilthlem3  27131  bcmono  27339  gausslemma2dlem1a  27427  sslttr  27870  ssltun1  27871  ssltun2  27872  sltlpss  27963  precsexlem8  28256  precsexlem9  28257  precsex  28260  expscl  28431  expsgt0  28433  pw2cut  28438  iscgrglt  28540  axcontlem7  29003  elntg2  29018  edglnl  29178  numedglnl  29179  ausgrumgri  29202  ausgrusgri  29203  usgrausgrb  29204  usgredg2vtxeuALT  29257  ushgredgedg  29264  ushgredgedgloop  29266  nbuhgr2vtx1edgb  29387  cusgrsize2inds  29489  upgrewlkle2  29642  wlkl1loop  29674  redwlk  29708  pthdivtx  29765  pthdadjvtx  29766  upgr2pthnlp  29768  upgrspthswlk  29774  clwlkl1loop  29819  wwlksnred  29925  wwlksnextbi  29927  elwwlks2ons3im  29987  umgrwwlks2on  29990  clwwlknwwlksn  30070  clwwlkinwwlk  30072  wwlksext2clwwlk  30089  1pthon2v  30185  uhgr3cyclex  30214  n4cyclfrgr  30323  frgrwopreg  30355  numclwwlk1lem2f1  30389  clwwlknonclwlknonf1o  30394  wlkl0  30399  frgrreggt1  30425  frgrreg  30426  frgrregord013  30427  chintcli  31363  spansnss  31603  elspansn4  31605  chscllem4  31672  hoadddir  31836  adjmul  32124  kbass6  32153  spansncv2  32325  sumdmdii  32447  nexple  33973  bnj1417  35017  lfuhgr2  35086  cusgredgex  35089  sat1el2xp  35347  fmlasuc  35354  satffunlem1lem1  35370  satffunlem2lem1  35372  mclsind  35538  iprodefisumlem  35702  btwndiff  35991  elicc3  36283  finminlem  36284  sdclem2  37702  clmgmOLD  37811  grpomndo  37835  zerdivemp1x  37907  lsmsat  38964  lsmcv2  38985  lcvat  38986  lsatcveq0  38988  lcvexchlem4  38993  lcvexchlem5  38994  islshpcv  39009  l1cvpat  39010  lshpkrlem6  39071  omlfh3N  39215  cvlsupr4  39301  cvlsupr5  39302  cvlsupr6  39303  2llnneN  39366  hlrelat3  39369  cvrval3  39370  cvrval4N  39371  cvrexchlem  39376  2atlt  39396  cvrat4  39400  atbtwnexOLDN  39404  atbtwnex  39405  athgt  39413  3dim1  39424  3dim2  39425  3dim3  39426  1cvratex  39430  llnle  39475  atcvrlln2  39476  atcvrlln  39477  2llnmat  39481  lplnle  39497  lplnnle2at  39498  lplnnlelln  39500  llncvrlpln2  39514  2llnjN  39524  lvoli2  39538  lvolnlelln  39541  lvolnlelpln  39542  4atlem10  39563  4atlem11  39566  4atlem12  39569  lplncvrlvol2  39572  2lplnj  39577  lneq2at  39735  lnatexN  39736  lnjatN  39737  lncvrat  39739  2lnat  39741  cdlemb  39751  paddasslem14  39790  llnexchb2  39826  dalawlem10  39837  dalawlem13  39840  dalawlem14  39841  dalaw  39843  pclclN  39848  pclfinN  39857  osumcllem11N  39923  lhp2lt  39958  lhpexle3lem  39968  4atexlem7  40032  ldilcnv  40072  ldilco  40073  ltrncnv  40103  trlval2  40120  cdleme24  40309  cdleme26ee  40317  cdleme28  40330  cdleme32le  40404  cdleme50trn2  40508  cdleme50ltrn  40514  cdleme  40517  cdlemf1  40518  cdlemf  40520  cdlemg1cex  40545  cdlemg2ce  40549  cdlemg18b  40636  ltrnco  40676  tendocan  40781  cdlemk28-3  40865  cdlemk11t  40903  dia2dimlem6  41026  dia2dimlem12  41032  dihlsscpre  41191  dihord4  41215  dihord5b  41216  dihmeetlem3N  41262  dihmeetlem20N  41283  dvh4dimlem  41400  lclkrlem2y  41488  mapdpglem24  41661  mapdpglem32  41662  mapdpg  41663  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  mapdh9a  41746  mapdh9aOLDN  41747  hdmap14lem6  41830  hdmapglem7  41886  indstrd  42150  nnadddir  42259  nnmulcom  42261  sn-addlid  42380  remulcand  42414  mzpexpmpt  42701  pellexlem5  42789  pellex  42791  pell14qrexpclnn0  42822  pellfundex  42842  monotuz  42898  monotoddzzfi  42899  rmxypos  42904  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.19lem3  42948  jm2.15nn0  42960  jm2.16nn0  42961  aomclem2  43012  aomclem6  43016  dfac11  43019  hbtlem5  43085  cnsrexpcl  43122  cantnf2  43287  dflim5  43291  relexpxpnnidm  43665  relexpiidm  43666  relexpss1d  43667  iunrelexpmin1  43670  relexpmulnn  43671  iunrelexpmin2  43674  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  trclimalb2  43688  tfindsd  44174  3impexpbicomi  44451  ee333  44478  eel12131  44684  eel2122old  44689  e333  44704  ordelordALTVD  44838  refsumcn  44930  uzwo4  44955  ssinc  44989  ssdec  44990  iunincfi  44996  restuni3  45020  eliuniin2  45022  rabssd  45044  reximdd  45053  suprnmpt  45081  disjf1o  45098  disjinfi  45099  ssnnf1octb  45101  choicefi  45107  mapssbi  45120  unirnmapsn  45121  ssmapsn  45123  iunmapsn  45124  rnmptlb  45152  rnmptbddlem  45153  infnsuprnmpt  45159  fperiodmullem  45218  upbdrech  45220  ssfiunibd  45224  supxrgere  45248  iuneqfzuzlem  45249  supxrgelem  45252  supxrge  45253  suplesup  45254  infrpge  45266  infleinf  45287  suplesup2  45291  supxrunb3  45314  infleinf2  45329  rexabslelem  45333  infrnmptle  45338  infxrunb3rnmpt  45343  iccshift  45436  iooshift  45440  fmul01  45501  fmuldfeq  45504  fmul01lt1  45507  mullimc  45537  islptre  45540  mullimcf  45544  limcperiod  45549  islpcn  45560  limsupre  45562  limcleqr  45565  neglimc  45568  addlimc  45569  0ellimcdiv  45570  limclner  45572  fnlimfvre  45595  limsuppnflem  45631  limsupmnfuzlem  45647  limsupre3lem  45653  limsupre3uzlem  45656  climuzlem  45664  limsupgtlem  45698  coskpi2  45787  cosknegpi  45790  cncfshift  45795  cncfperiod  45800  icccncfext  45808  dvnmptdivc  45859  dvnmptconst  45862  dvnmul  45864  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  itgperiod  45902  ismbl3  45907  stoweidlem3  45924  stoweidlem31  45952  stoweidlem59  45980  stirlinglem13  46007  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem51  46078  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem80  46107  fourierdlem81  46108  fourierdlem89  46116  fourierdlem91  46118  fourierdlem93  46120  fourierdlem97  46124  elaa2  46155  qndenserrnopnlem  46218  salexct  46255  subsaliuncl  46279  subsalsal  46280  sge0tsms  46301  sge0f1o  46303  sge0fsum  46308  sge0supre  46310  sge0sup  46312  sge0rnbnd  46314  sge0gerp  46316  sge0pnffigt  46317  sge0lefi  46319  sge0ltfirp  46321  sge0resrn  46325  sge0resplit  46327  sge0split  46330  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0rpcpnf  46342  sge0isum  46348  sge0xp  46350  sge0xaddlem2  46355  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  nnfoctbdjlem  46376  nnfoctbdj  46377  iundjiun  46381  meadjiunlem  46386  voliunsge0lem  46393  meaiuninclem  46401  meaiininc2  46409  carageniuncllem1  46442  carageniuncllem2  46443  caratheodorylem1  46447  caratheodorylem2  46448  isomenndlem  46451  ovnsupge0  46478  ovnlerp  46483  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmvval0  46508  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem2  46523  opnvonmbllem2  46554  ovnovollem3  46579  vonioo  46603  vonicc  46606  pimiooltgt  46631  sssmf  46659  smfaddlem1  46684  smflimlem6  46697  smfmullem4  46715  smfpimbor1lem1  46719  smfco  46723  smfpimcc  46729  smflimmpt  46731  smfinflem  46738  smflimsuplem7  46747  smflimsuplem8  46748  smflimsupmpt  46750  smfliminfmpt  46753  cfsetsnfsetf1  46974  elsetpreimafveqfv  47266  iccpartiltu  47296  sprsymrelfvlem  47364  reuopreuprim  47400  goldbachth  47421  fmtnofac1  47444  prmdvdsfmtnof1lem1  47458  lighneal  47485  grimuhgr  47762  uhgrimisgrgriclem  47782  clnbgrgrim  47786  grimedg  47787  usgrgrtrirex  47799  uspgrlimlem2  47813  grlimgrtri  47820  grlicsym  47830  uspgropssxp  47867  rngccatidALTV  47995  ringccatidALTV  48029  lcosslsp  48167  fllog2  48302  dignn0flhalf  48352  fv1arycl  48371  1arymaptf1  48376  fv2arycl  48382  2arymaptf1  48387  itschlc0yqe  48494  itsclc0xyqsol  48502  seposep  48605  iscnrm3lem6  48618  iunord  48768  setrec2fun  48784