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  3141  rabssdv  4026  reupick2  4283  disjiund  5089  otiunsndisj  5468  wefrc  5618  tz7.7  6343  unizlim  6441  funimassd  6900  fvelimad  6901  fveqdmss  7023  fompt  7063  f1oiso2  7298  ssorduni  7724  tfisi  7801  resf1extb  7876  funeldmdif  7992  poxp  8070  poseq  8100  fpr3g  8227  frrlem10  8237  smo11  8296  tfrlem5  8311  odi  8506  omass  8507  nndi  8551  nnmass  8552  naddoa  8630  undifixp  8872  findcard  9088  php3  9133  ac6sfi  9184  domunfican  9222  mapfien2  9312  fisup2g  9372  fiinf2g  9405  ttrclss  9629  ttrclselem2  9635  indcardi  9951  acndom  9961  ackbij1lem16  10144  infpssrlem4  10216  fin23lem11  10227  isfin2-2  10229  fin23lem34  10256  fin1a2lem10  10319  hsmexlem2  10337  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axcclem  10367  ttukeyg  10427  axdclem2  10430  axacndlem4  10521  axacndlem5  10522  axacnd  10523  tskr1om2  10679  tskwe2  10684  tskord  10691  tskcard  10692  tskuni  10694  tskwun  10695  gruiin  10721  grudomon  10728  gruina  10729  mulcanpi  10811  adderpq  10867  mulerpq  10868  dedekindle  11297  divgt0  12010  divge0  12011  nnne0  12179  uzind  12584  uzind2  12585  iccsplit  13401  ssnn0fi  13908  expmordi  14090  sqlecan  14132  modexp  14161  expnngt1  14164  facavg  14224  2cshwcshw  14748  relexpcnv  14958  relexpaddnn  14974  relexpaddg  14976  pwdif  15791  prodfn0  15817  prodfrec  15818  ntrivcvgfvn0  15822  fprodabs  15897  bpolycl  15975  bpolydif  15978  fprodefsum  16018  dvdsmodexp  16187  dvdsaddre2b  16234  nn0rppwr  16488  dvdsnprmd  16617  2mulprm  16620  prmndvdsfaclt  16652  ncoprmlnprm  16655  fermltl  16711  pceu  16774  setsstruct2  17101  setsstruct  17103  mreexexd  17571  isglbd  18432  symgpssefmnd  19325  pmtrfrn  19387  psgnunilem4  19426  ablsimpgprmd  20046  mulgass2  20244  islss4  20913  lspsneu  21078  lspfixed  21083  lspexch  21084  lsmcv  21096  lspsolvlem  21097  rnglidlmcl  21171  xrsdsreclblem  21367  nzerooringczr  21435  isphld  21609  mdetralt  22552  mdetunilem9  22564  fiinopn  22845  neips  23057  tpnei  23065  neindisj2  23067  opnneiid  23070  hausnei2  23297  cmpsublem  23343  cmpsub  23344  cmpcld  23346  comppfsc  23476  filufint  23864  cfinufil  23872  rnelfm  23897  alexsubALTlem1  23991  alexsubALTlem4  23994  alexsubALT  23995  tsmsxp  24099  neibl  24445  tngngp3  24600  tgqioo  24744  ovolunlem2  25455  iunmbl2  25514  itg1le  25670  vieta1  26276  aannenlem2  26293  aalioulem3  26298  aalioulem4  26299  aaliou2  26304  wilthlem3  27036  bcmono  27244  gausslemma2dlem1a  27332  sltstr  27783  sltsun1  27784  sltsun2  27785  ltslpss  27904  precsexlem8  28210  precsexlem9  28211  precsex  28214  onsfi  28352  oldfib  28373  expscllem  28426  expsgt0  28433  pw2cut  28456  pw2cut2  28458  bdaypw2n0bnd  28460  bdayfin  28483  iscgrglt  28586  axcontlem7  29043  elntg2  29058  edglnl  29216  numedglnl  29217  ausgrumgri  29240  ausgrusgri  29241  usgrausgrb  29242  usgredg2vtxeuALT  29295  ushgredgedg  29302  ushgredgedgloop  29304  nbuhgr2vtx1edgb  29425  cusgrsize2inds  29527  upgrewlkle2  29680  wlkl1loop  29711  redwlk  29744  pthdivtx  29800  pthdadjvtx  29801  upgr2pthnlp  29805  upgrspthswlk  29811  clwlkl1loop  29856  cyclnumvtx  29873  wwlksnred  29965  wwlksnextbi  29967  elwwlks2ons3im  30027  usgrwwlks2on  30031  umgrwwlks2on  30032  clwwlknwwlksn  30113  clwwlkinwwlk  30115  wwlksext2clwwlk  30132  1pthon2v  30228  uhgr3cyclex  30257  n4cyclfrgr  30366  frgrwopreg  30398  numclwwlk1lem2f1  30432  clwwlknonclwlknonf1o  30437  wlkl0  30442  frgrreggt1  30468  frgrreg  30469  frgrregord013  30470  chintcli  31406  spansnss  31646  elspansn4  31648  chscllem4  31715  hoadddir  31879  adjmul  32167  kbass6  32196  spansncv2  32368  sumdmdii  32490  nexple  32925  bnj1417  35197  lfuhgr2  35313  cusgredgex  35316  sat1el2xp  35573  fmlasuc  35580  satffunlem1lem1  35596  satffunlem2lem1  35598  mclsind  35764  iprodefisumlem  35934  btwndiff  36221  elicc3  36511  finminlem  36512  sdclem2  37943  clmgmOLD  38052  grpomndo  38076  zerdivemp1x  38148  lsmsat  39268  lsmcv2  39289  lcvat  39290  lsatcveq0  39292  lcvexchlem4  39297  lcvexchlem5  39298  islshpcv  39313  l1cvpat  39314  lshpkrlem6  39375  omlfh3N  39519  cvlsupr4  39605  cvlsupr5  39606  cvlsupr6  39607  2llnneN  39669  hlrelat3  39672  cvrval3  39673  cvrval4N  39674  cvrexchlem  39679  2atlt  39699  cvrat4  39703  atbtwnexOLDN  39707  atbtwnex  39708  athgt  39716  3dim1  39727  3dim2  39728  3dim3  39729  1cvratex  39733  llnle  39778  atcvrlln2  39779  atcvrlln  39780  2llnmat  39784  lplnle  39800  lplnnle2at  39801  lplnnlelln  39803  llncvrlpln2  39817  2llnjN  39827  lvoli2  39841  lvolnlelln  39844  lvolnlelpln  39845  4atlem10  39866  4atlem11  39869  4atlem12  39872  lplncvrlvol2  39875  2lplnj  39880  lneq2at  40038  lnatexN  40039  lnjatN  40040  lncvrat  40042  2lnat  40044  cdlemb  40054  paddasslem14  40093  llnexchb2  40129  dalawlem10  40140  dalawlem13  40143  dalawlem14  40144  dalaw  40146  pclclN  40151  pclfinN  40160  osumcllem11N  40226  lhp2lt  40261  lhpexle3lem  40271  4atexlem7  40335  ldilcnv  40375  ldilco  40376  ltrncnv  40406  trlval2  40423  cdleme24  40612  cdleme26ee  40620  cdleme28  40633  cdleme32le  40707  cdleme50trn2  40811  cdleme50ltrn  40817  cdleme  40820  cdlemf1  40821  cdlemf  40823  cdlemg1cex  40848  cdlemg2ce  40852  cdlemg18b  40939  ltrnco  40979  tendocan  41084  cdlemk28-3  41168  cdlemk11t  41206  dia2dimlem6  41329  dia2dimlem12  41335  dihlsscpre  41494  dihord4  41518  dihord5b  41519  dihmeetlem3N  41565  dihmeetlem20N  41586  dvh4dimlem  41703  lclkrlem2y  41791  mapdpglem24  41964  mapdpglem32  41965  mapdpg  41966  baerlem3lem2  41970  baerlem5alem2  41971  baerlem5blem2  41972  mapdh9a  42049  mapdh9aOLDN  42050  hdmap14lem6  42133  hdmapglem7  42189  indstrd  42447  nnadddir  42525  nnmulcom  42527  sn-addlid  42659  remulcand  42694  mzpexpmpt  42987  pellexlem5  43075  pellex  43077  pell14qrexpclnn0  43108  pellfundex  43128  monotuz  43183  monotoddzzfi  43184  rmxypos  43189  jm2.17a  43202  jm2.17b  43203  rmygeid  43206  jm2.19lem3  43233  jm2.15nn0  43245  jm2.16nn0  43246  aomclem2  43297  aomclem6  43301  dfac11  43304  hbtlem5  43370  cnsrexpcl  43407  cantnf2  43567  dflim5  43571  relexpxpnnidm  43944  relexpiidm  43945  relexpss1d  43946  iunrelexpmin1  43949  relexpmulnn  43950  iunrelexpmin2  43953  relexp01min  43954  relexp0a  43957  relexpxpmin  43958  relexpaddss  43959  trclimalb2  43967  tfindsd  44451  3impexpbicomi  44722  ee333  44748  eel12131  44953  eel2122old  44958  e333  44973  ordelordALTVD  45107  refsumcn  45275  uzwo4  45298  ssinc  45331  ssdec  45332  iunincfi  45338  restuni3  45362  eliuniin2  45364  rabssd  45386  reximdd  45392  suprnmpt  45418  disjf1o  45435  disjinfi  45436  ssnnf1octb  45438  choicefi  45444  mapssbi  45457  unirnmapsn  45458  iunmapsn  45461  rnmptlb  45487  rnmptbddlem  45488  infnsuprnmpt  45494  fperiodmullem  45551  upbdrech  45553  ssfiunibd  45557  supxrgere  45578  iuneqfzuzlem  45579  supxrgelem  45582  supxrge  45583  suplesup  45584  infrpge  45596  infleinf  45616  suplesup2  45620  supxrunb3  45643  infleinf2  45658  rexabslelem  45662  infrnmptle  45667  infxrunb3rnmpt  45672  iccshift  45764  iooshift  45768  fmul01  45826  fmuldfeq  45829  fmul01lt1  45832  mullimc  45862  islptre  45865  mullimcf  45869  limcperiod  45874  islpcn  45883  limsupre  45885  limcleqr  45888  neglimc  45891  addlimc  45892  0ellimcdiv  45893  limclner  45895  fnlimfvre  45918  limsuppnflem  45954  limsupmnfuzlem  45970  limsupre3lem  45976  limsupre3uzlem  45979  climuzlem  45987  limsupgtlem  46021  coskpi2  46110  cosknegpi  46113  cncfshift  46118  cncfperiod  46123  icccncfext  46131  dvnmptdivc  46182  dvnmptconst  46185  dvnmul  46187  dvmptfprodlem  46188  dvmptfprod  46189  dvnprodlem1  46190  dvnprodlem2  46191  iblspltprt  46217  itgspltprt  46223  itgperiod  46225  ismbl3  46230  stoweidlem3  46247  stoweidlem31  46275  stoweidlem59  46303  stirlinglem13  46330  fourierdlem41  46392  fourierdlem42  46393  fourierdlem48  46398  fourierdlem51  46401  fourierdlem70  46420  fourierdlem71  46421  fourierdlem73  46423  fourierdlem80  46430  fourierdlem81  46431  fourierdlem89  46439  fourierdlem91  46441  fourierdlem93  46443  fourierdlem97  46447  elaa2  46478  qndenserrnopnlem  46541  salexct  46578  subsaliuncl  46602  subsalsal  46603  sge0tsms  46624  sge0f1o  46626  sge0fsum  46631  sge0supre  46633  sge0sup  46635  sge0rnbnd  46637  sge0gerp  46639  sge0pnffigt  46640  sge0lefi  46642  sge0ltfirp  46644  sge0resrn  46648  sge0resplit  46650  sge0split  46653  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0rpcpnf  46665  sge0isum  46671  sge0xp  46673  sge0xaddlem2  46678  sge0uzfsumgt  46688  sge0seq  46690  sge0reuz  46691  nnfoctbdjlem  46699  nnfoctbdj  46700  iundjiun  46704  meadjiunlem  46709  voliunsge0lem  46716  meaiuninclem  46724  meaiininc2  46732  carageniuncllem1  46765  carageniuncllem2  46766  caratheodorylem1  46770  caratheodorylem2  46771  isomenndlem  46774  ovnsupge0  46801  ovnlerp  46806  ovncvrrp  46808  ovnsubaddlem1  46814  hoidmvval0  46831  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  ovnhoilem2  46846  opnvonmbllem2  46877  ovnovollem3  46902  vonioo  46926  vonicc  46929  pimiooltgt  46954  sssmf  46982  smfaddlem1  47007  smflimlem6  47020  smfmullem4  47038  smfpimbor1lem1  47042  smfco  47046  smfpimcc  47052  smflimmpt  47054  smfinflem  47061  smflimsuplem7  47070  smflimsuplem8  47071  smflimsupmpt  47073  smfliminfmpt  47076  cfsetsnfsetf1  47305  2tceilhalfelfzo1  47578  elsetpreimafveqfv  47638  iccpartiltu  47668  sprsymrelfvlem  47736  reuopreuprim  47772  goldbachth  47793  fmtnofac1  47816  prmdvdsfmtnof1lem1  47830  lighneal  47857  grimuhgr  48133  uhgrimedgi  48136  uhgrimisgrgriclem  48176  clnbgrgrim  48180  grimedg  48181  usgrgrtrirex  48196  isubgr3stgrlem3  48214  isubgr3stgrlem6  48217  uspgrlimlem2  48235  grlimgrtri  48249  grlicsym  48259  clnbgr3stgrgrlic  48266  gpgusgralem  48302  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  uspgropssxp  48390  rngccatidALTV  48518  ringccatidALTV  48552  lcosslsp  48684  fllog2  48814  dignn0flhalf  48864  fv1arycl  48883  1arymaptf1  48888  fv2arycl  48894  2arymaptf1  48899  itschlc0yqe  49006  itsclc0xyqsol  49014  seposep  49171  iscnrm3lem6  49183  iunord  49921  setrec2fun  49937