Theorem 3exp 1120

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 1119	. 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  1121  3expib  1123  3com12  1124  3com13  1125  pm3.2an3  1342  3exp1  1354  3expd  1355  exp5o  1357  3ecase  1477  rexlimdv3a  3143  rabssdv  4015  reupick2  4272  disjiund  5077  otiunsndisj  5468  wefrc  5618  tz7.7  6343  unizlim  6441  funimassd  6900  fvelimad  6901  fveqdmss  7024  fompt  7064  f1oiso2  7300  ssorduni  7726  tfisi  7803  resf1extb  7878  funeldmdif  7994  poxp  8071  poseq  8101  fpr3g  8228  frrlem10  8238  smo11  8297  tfrlem5  8312  odi  8507  omass  8508  nndi  8552  nnmass  8553  naddoa  8631  undifixp  8875  findcard  9091  php3  9136  ac6sfi  9187  domunfican  9225  mapfien2  9315  fisup2g  9375  fiinf2g  9408  ttrclss  9632  ttrclselem2  9638  indcardi  9954  acndom  9964  ackbij1lem16  10147  infpssrlem4  10219  fin23lem11  10230  isfin2-2  10232  fin23lem34  10259  fin1a2lem10  10322  hsmexlem2  10340  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axcclem  10370  ttukeyg  10430  axdclem2  10433  axacndlem4  10524  axacndlem5  10525  axacnd  10526  tskr1om2  10682  tskwe2  10687  tskord  10694  tskcard  10695  tskuni  10697  tskwun  10698  gruiin  10724  grudomon  10731  gruina  10732  mulcanpi  10814  adderpq  10870  mulerpq  10871  dedekindle  11301  divgt0  12015  divge0  12016  nnne0  12202  nnadddir  12224  nnmulcom  12226  uzind  12612  uzind2  12613  iccsplit  13429  ssnn0fi  13938  expmordi  14120  sqlecan  14162  modexp  14191  expnngt1  14194  facavg  14254  2cshwcshw  14778  relexpcnv  14988  relexpaddnn  15004  relexpaddg  15006  pwdif  15824  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  fprodabs  15930  bpolycl  16008  bpolydif  16011  fprodefsum  16051  dvdsmodexp  16220  dvdsaddre2b  16267  nn0rppwr  16521  dvdsnprmd  16650  2mulprm  16653  prmndvdsfaclt  16686  ncoprmlnprm  16689  fermltl  16745  pceu  16808  setsstruct2  17135  setsstruct  17137  mreexexd  17605  isglbd  18466  symgpssefmnd  19362  pmtrfrn  19424  psgnunilem4  19463  ablsimpgprmd  20083  mulgass2  20281  islss4  20948  lspsneu  21113  lspfixed  21118  lspexch  21119  lsmcv  21131  lspsolvlem  21132  rnglidlmcl  21206  xrsdsreclblem  21402  nzerooringczr  21470  isphld  21644  mdetralt  22583  mdetunilem9  22595  fiinopn  22876  neips  23088  tpnei  23096  neindisj2  23098  opnneiid  23101  hausnei2  23328  cmpsublem  23374  cmpsub  23375  cmpcld  23377  comppfsc  23507  filufint  23895  cfinufil  23903  rnelfm  23928  alexsubALTlem1  24022  alexsubALTlem4  24025  alexsubALT  24026  tsmsxp  24130  neibl  24476  tngngp3  24631  tgqioo  24775  ovolunlem2  25475  iunmbl2  25534  itg1le  25690  vieta1  26289  aannenlem2  26306  aalioulem3  26311  aalioulem4  26312  aaliou2  26317  wilthlem3  27047  bcmono  27254  gausslemma2dlem1a  27342  sltstr  27793  sltsun1  27794  sltsun2  27795  ltslpss  27914  precsexlem8  28220  precsexlem9  28221  precsex  28224  onsfi  28362  oldfib  28383  expscllem  28436  expsgt0  28443  pw2cut  28466  pw2cut2  28468  bdaypw2n0bnd  28470  bdayfin  28493  iscgrglt  28596  axcontlem7  29053  elntg2  29068  edglnl  29226  numedglnl  29227  ausgrumgri  29250  ausgrusgri  29251  usgrausgrb  29252  usgredg2vtxeuALT  29305  ushgredgedg  29312  ushgredgedgloop  29314  nbuhgr2vtx1edgb  29435  cusgrsize2inds  29537  upgrewlkle2  29690  wlkl1loop  29721  redwlk  29754  pthdivtx  29810  pthdadjvtx  29811  upgr2pthnlp  29815  upgrspthswlk  29821  clwlkl1loop  29866  cyclnumvtx  29883  wwlksnred  29975  wwlksnextbi  29977  elwwlks2ons3im  30037  usgrwwlks2on  30041  umgrwwlks2on  30042  clwwlknwwlksn  30123  clwwlkinwwlk  30125  wwlksext2clwwlk  30142  1pthon2v  30238  uhgr3cyclex  30267  n4cyclfrgr  30376  frgrwopreg  30408  numclwwlk1lem2f1  30442  clwwlknonclwlknonf1o  30447  wlkl0  30452  frgrreggt1  30478  frgrreg  30479  frgrregord013  30480  chintcli  31417  spansnss  31657  elspansn4  31659  chscllem4  31726  hoadddir  31890  adjmul  32178  kbass6  32207  spansncv2  32379  sumdmdii  32501  nexple  32932  bnj1417  35199  lfuhgr2  35317  cusgredgex  35320  sat1el2xp  35577  fmlasuc  35584  satffunlem1lem1  35600  satffunlem2lem1  35602  mclsind  35768  iprodefisumlem  35938  btwndiff  36225  elicc3  36515  finminlem  36516  axtcond  36676  ttcmin  36694  sdclem2  38077  clmgmOLD  38186  grpomndo  38210  zerdivemp1x  38282  lsmsat  39468  lsmcv2  39489  lcvat  39490  lsatcveq0  39492  lcvexchlem4  39497  lcvexchlem5  39498  islshpcv  39513  l1cvpat  39514  lshpkrlem6  39575  omlfh3N  39719  cvlsupr4  39805  cvlsupr5  39806  cvlsupr6  39807  2llnneN  39869  hlrelat3  39872  cvrval3  39873  cvrval4N  39874  cvrexchlem  39879  2atlt  39899  cvrat4  39903  atbtwnexOLDN  39907  atbtwnex  39908  athgt  39916  3dim1  39927  3dim2  39928  3dim3  39929  1cvratex  39933  llnle  39978  atcvrlln2  39979  atcvrlln  39980  2llnmat  39984  lplnle  40000  lplnnle2at  40001  lplnnlelln  40003  llncvrlpln2  40017  2llnjN  40027  lvoli2  40041  lvolnlelln  40044  lvolnlelpln  40045  4atlem10  40066  4atlem11  40069  4atlem12  40072  lplncvrlvol2  40075  2lplnj  40080  lneq2at  40238  lnatexN  40239  lnjatN  40240  lncvrat  40242  2lnat  40244  cdlemb  40254  paddasslem14  40293  llnexchb2  40329  dalawlem10  40340  dalawlem13  40343  dalawlem14  40344  dalaw  40346  pclclN  40351  pclfinN  40360  osumcllem11N  40426  lhp2lt  40461  lhpexle3lem  40471  4atexlem7  40535  ldilcnv  40575  ldilco  40576  ltrncnv  40606  trlval2  40623  cdleme24  40812  cdleme26ee  40820  cdleme28  40833  cdleme32le  40907  cdleme50trn2  41011  cdleme50ltrn  41017  cdleme  41020  cdlemf1  41021  cdlemf  41023  cdlemg1cex  41048  cdlemg2ce  41052  cdlemg18b  41139  ltrnco  41179  tendocan  41284  cdlemk28-3  41368  cdlemk11t  41406  dia2dimlem6  41529  dia2dimlem12  41535  dihlsscpre  41694  dihord4  41718  dihord5b  41719  dihmeetlem3N  41765  dihmeetlem20N  41786  dvh4dimlem  41903  lclkrlem2y  41991  mapdpglem24  42164  mapdpglem32  42165  mapdpg  42166  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  mapdh9a  42249  mapdh9aOLDN  42250  hdmap14lem6  42333  hdmapglem7  42389  indstrd  42646  sn-addlid  42850  remulcand  42885  mzpexpmpt  43191  pellexlem5  43279  pellex  43281  pell14qrexpclnn0  43312  pellfundex  43332  monotuz  43387  monotoddzzfi  43388  rmxypos  43393  jm2.17a  43406  jm2.17b  43407  rmygeid  43410  jm2.19lem3  43437  jm2.15nn0  43449  jm2.16nn0  43450  aomclem2  43501  aomclem6  43505  dfac11  43508  hbtlem5  43574  cnsrexpcl  43611  cantnf2  43771  dflim5  43775  relexpxpnnidm  44148  relexpiidm  44149  relexpss1d  44150  iunrelexpmin1  44153  relexpmulnn  44154  iunrelexpmin2  44157  relexp01min  44158  relexp0a  44161  relexpxpmin  44162  relexpaddss  44163  trclimalb2  44171  tfindsd  44655  3impexpbicomi  44926  ee333  44952  eel12131  45157  eel2122old  45162  e333  45177  ordelordALTVD  45311  refsumcn  45479  uzwo4  45502  ssinc  45535  ssdec  45536  iunincfi  45542  restuni3  45566  eliuniin2  45568  rabssd  45590  reximdd  45596  suprnmpt  45622  disjf1o  45639  disjinfi  45640  ssnnf1octb  45642  choicefi  45647  mapssbi  45660  unirnmapsn  45661  iunmapsn  45664  rnmptlb  45690  rnmptbddlem  45691  infnsuprnmpt  45697  fperiodmullem  45754  upbdrech  45756  ssfiunibd  45760  supxrgere  45781  iuneqfzuzlem  45782  supxrgelem  45785  supxrge  45786  suplesup  45787  infrpge  45799  infleinf  45819  suplesup2  45823  supxrunb3  45846  infleinf2  45860  rexabslelem  45864  infrnmptle  45869  infxrunb3rnmpt  45874  iccshift  45966  iooshift  45970  fmul01  46028  fmuldfeq  46031  fmul01lt1  46034  mullimc  46064  islptre  46067  mullimcf  46071  limcperiod  46076  islpcn  46085  limsupre  46087  limcleqr  46090  neglimc  46093  addlimc  46094  0ellimcdiv  46095  limclner  46097  fnlimfvre  46120  limsuppnflem  46156  limsupmnfuzlem  46172  limsupre3lem  46178  limsupre3uzlem  46181  climuzlem  46189  limsupgtlem  46223  coskpi2  46312  cosknegpi  46315  cncfshift  46320  cncfperiod  46325  icccncfext  46333  dvnmptdivc  46384  dvnmptconst  46387  dvnmul  46389  dvmptfprodlem  46390  dvmptfprod  46391  dvnprodlem1  46392  dvnprodlem2  46393  iblspltprt  46419  itgspltprt  46425  itgperiod  46427  ismbl3  46432  stoweidlem3  46449  stoweidlem31  46477  stoweidlem59  46505  stirlinglem13  46532  fourierdlem41  46594  fourierdlem42  46595  fourierdlem48  46600  fourierdlem51  46603  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem80  46632  fourierdlem81  46633  fourierdlem89  46641  fourierdlem91  46643  fourierdlem93  46645  fourierdlem97  46649  elaa2  46680  qndenserrnopnlem  46743  salexct  46780  subsaliuncl  46804  subsalsal  46805  sge0tsms  46826  sge0f1o  46828  sge0fsum  46833  sge0supre  46835  sge0sup  46837  sge0rnbnd  46839  sge0gerp  46841  sge0pnffigt  46842  sge0lefi  46844  sge0ltfirp  46846  sge0resrn  46850  sge0resplit  46852  sge0split  46855  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0rpcpnf  46867  sge0isum  46873  sge0xp  46875  sge0xaddlem2  46880  sge0uzfsumgt  46890  sge0seq  46892  sge0reuz  46893  nnfoctbdjlem  46901  nnfoctbdj  46902  iundjiun  46906  meadjiunlem  46911  voliunsge0lem  46918  meaiuninclem  46926  meaiininc2  46934  carageniuncllem1  46967  carageniuncllem2  46968  caratheodorylem1  46972  caratheodorylem2  46973  isomenndlem  46976  ovnsupge0  47003  ovnlerp  47008  ovncvrrp  47010  ovnsubaddlem1  47016  hoidmvval0  47033  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem2  47048  opnvonmbllem2  47079  ovnovollem3  47104  vonioo  47128  vonicc  47131  pimiooltgt  47156  sssmf  47184  smfaddlem1  47209  smflimlem6  47222  smfmullem4  47240  smfpimbor1lem1  47244  smfco  47248  smfpimcc  47254  smflimmpt  47256  smfinflem  47263  smflimsuplem7  47272  smflimsuplem8  47273  smflimsupmpt  47275  smfliminfmpt  47278  cfsetsnfsetf1  47519  nnmul2b  47791  2tceilhalfelfzo1  47796  elsetpreimafveqfv  47864  iccpartiltu  47894  sprsymrelfvlem  47962  reuopreuprim  47998  nprmmul2  48000  goldbachth  48022  fmtnofac1  48045  prmdvdsfmtnof1lem1  48059  lighneal  48086  grimuhgr  48375  uhgrimedgi  48378  uhgrimisgrgriclem  48418  clnbgrgrim  48422  grimedg  48423  usgrgrtrirex  48438  isubgr3stgrlem3  48456  isubgr3stgrlem6  48459  uspgrlimlem2  48477  grlimgrtri  48491  grlicsym  48501  clnbgr3stgrgrlic  48508  gpgusgralem  48544  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  uspgropssxp  48632  rngccatidALTV  48760  ringccatidALTV  48794  lcosslsp  48926  fllog2  49056  dignn0flhalf  49106  fv1arycl  49125  1arymaptf1  49130  fv2arycl  49136  2arymaptf1  49141  itschlc0yqe  49248  itsclc0xyqsol  49256  seposep  49413  iscnrm3lem6  49425  iunord  50163  setrec2fun  50179