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  3138  rabssdv  4023  reupick2  4280  disjiund  5086  otiunsndisj  5465  wefrc  5615  tz7.7  6340  unizlim  6438  funimassd  6897  fvelimad  6898  fveqdmss  7020  fompt  7060  f1oiso2  7295  ssorduni  7721  tfisi  7798  resf1extb  7873  funeldmdif  7989  poxp  8067  poseq  8097  fpr3g  8224  frrlem10  8234  smo11  8293  tfrlem5  8308  odi  8503  omass  8504  nndi  8547  nnmass  8548  naddoa  8626  undifixp  8868  findcard  9084  php3  9129  ac6sfi  9179  domunfican  9217  mapfien2  9304  fisup2g  9364  fiinf2g  9397  ttrclss  9621  ttrclselem2  9627  indcardi  9943  acndom  9953  ackbij1lem16  10136  infpssrlem4  10208  fin23lem11  10219  isfin2-2  10221  fin23lem34  10248  fin1a2lem10  10311  hsmexlem2  10329  axcc3  10340  domtriomlem  10344  axdc3lem2  10353  axdc3lem4  10355  axcclem  10359  ttukeyg  10419  axdclem2  10422  axacndlem4  10512  axacndlem5  10513  axacnd  10514  tskr1om2  10670  tskwe2  10675  tskord  10682  tskcard  10683  tskuni  10685  tskwun  10686  gruiin  10712  grudomon  10719  gruina  10720  mulcanpi  10802  adderpq  10858  mulerpq  10859  dedekindle  11288  divgt0  12001  divge0  12002  nnne0  12170  uzind  12575  uzind2  12576  iccsplit  13392  ssnn0fi  13899  expmordi  14081  sqlecan  14123  modexp  14152  expnngt1  14155  facavg  14215  2cshwcshw  14739  relexpcnv  14949  relexpaddnn  14965  relexpaddg  14967  pwdif  15782  prodfn0  15808  prodfrec  15809  ntrivcvgfvn0  15813  fprodabs  15888  bpolycl  15966  bpolydif  15969  fprodefsum  16009  dvdsmodexp  16178  dvdsaddre2b  16225  nn0rppwr  16479  dvdsnprmd  16608  2mulprm  16611  prmndvdsfaclt  16643  ncoprmlnprm  16646  fermltl  16702  pceu  16765  setsstruct2  17092  setsstruct  17094  mreexexd  17562  isglbd  18423  symgpssefmnd  19316  pmtrfrn  19378  psgnunilem4  19417  ablsimpgprmd  20037  mulgass2  20235  islss4  20904  lspsneu  21069  lspfixed  21074  lspexch  21075  lsmcv  21087  lspsolvlem  21088  rnglidlmcl  21162  xrsdsreclblem  21358  nzerooringczr  21426  isphld  21600  mdetralt  22543  mdetunilem9  22555  fiinopn  22836  neips  23048  tpnei  23056  neindisj2  23058  opnneiid  23061  hausnei2  23288  cmpsublem  23334  cmpsub  23335  cmpcld  23337  comppfsc  23467  filufint  23855  cfinufil  23863  rnelfm  23888  alexsubALTlem1  23982  alexsubALTlem4  23985  alexsubALT  23986  tsmsxp  24090  neibl  24436  tngngp3  24591  tgqioo  24735  ovolunlem2  25446  iunmbl2  25505  itg1le  25661  vieta1  26267  aannenlem2  26284  aalioulem3  26289  aalioulem4  26290  aaliou2  26295  wilthlem3  27027  bcmono  27235  gausslemma2dlem1a  27323  sslttr  27768  ssltun1  27769  ssltun2  27770  sltlpss  27873  precsexlem8  28172  precsexlem9  28173  precsex  28176  onsfi  28303  expscllem  28373  expsgt0  28380  pw2cut  28400  pw2cut2  28402  iscgrglt  28512  axcontlem7  28969  elntg2  28984  edglnl  29142  numedglnl  29143  ausgrumgri  29166  ausgrusgri  29167  usgrausgrb  29168  usgredg2vtxeuALT  29221  ushgredgedg  29228  ushgredgedgloop  29230  nbuhgr2vtx1edgb  29351  cusgrsize2inds  29453  upgrewlkle2  29606  wlkl1loop  29637  redwlk  29670  pthdivtx  29726  pthdadjvtx  29727  upgr2pthnlp  29731  upgrspthswlk  29737  clwlkl1loop  29782  cyclnumvtx  29799  wwlksnred  29891  wwlksnextbi  29893  elwwlks2ons3im  29953  usgrwwlks2on  29957  umgrwwlks2on  29958  clwwlknwwlksn  30039  clwwlkinwwlk  30041  wwlksext2clwwlk  30058  1pthon2v  30154  uhgr3cyclex  30183  n4cyclfrgr  30292  frgrwopreg  30324  numclwwlk1lem2f1  30358  clwwlknonclwlknonf1o  30363  wlkl0  30368  frgrreggt1  30394  frgrreg  30395  frgrregord013  30396  chintcli  31332  spansnss  31572  elspansn4  31574  chscllem4  31641  hoadddir  31805  adjmul  32093  kbass6  32122  spansncv2  32294  sumdmdii  32416  nexple  32853  bnj1417  35125  lfuhgr2  35235  cusgredgex  35238  sat1el2xp  35495  fmlasuc  35502  satffunlem1lem1  35518  satffunlem2lem1  35520  mclsind  35686  iprodefisumlem  35856  btwndiff  36143  elicc3  36433  finminlem  36434  sdclem2  37855  clmgmOLD  37964  grpomndo  37988  zerdivemp1x  38060  lsmsat  39180  lsmcv2  39201  lcvat  39202  lsatcveq0  39204  lcvexchlem4  39209  lcvexchlem5  39210  islshpcv  39225  l1cvpat  39226  lshpkrlem6  39287  omlfh3N  39431  cvlsupr4  39517  cvlsupr5  39518  cvlsupr6  39519  2llnneN  39581  hlrelat3  39584  cvrval3  39585  cvrval4N  39586  cvrexchlem  39591  2atlt  39611  cvrat4  39615  atbtwnexOLDN  39619  atbtwnex  39620  athgt  39628  3dim1  39639  3dim2  39640  3dim3  39641  1cvratex  39645  llnle  39690  atcvrlln2  39691  atcvrlln  39692  2llnmat  39696  lplnle  39712  lplnnle2at  39713  lplnnlelln  39715  llncvrlpln2  39729  2llnjN  39739  lvoli2  39753  lvolnlelln  39756  lvolnlelpln  39757  4atlem10  39778  4atlem11  39781  4atlem12  39784  lplncvrlvol2  39787  2lplnj  39792  lneq2at  39950  lnatexN  39951  lnjatN  39952  lncvrat  39954  2lnat  39956  cdlemb  39966  paddasslem14  40005  llnexchb2  40041  dalawlem10  40052  dalawlem13  40055  dalawlem14  40056  dalaw  40058  pclclN  40063  pclfinN  40072  osumcllem11N  40138  lhp2lt  40173  lhpexle3lem  40183  4atexlem7  40247  ldilcnv  40287  ldilco  40288  ltrncnv  40318  trlval2  40335  cdleme24  40524  cdleme26ee  40532  cdleme28  40545  cdleme32le  40619  cdleme50trn2  40723  cdleme50ltrn  40729  cdleme  40732  cdlemf1  40733  cdlemf  40735  cdlemg1cex  40760  cdlemg2ce  40764  cdlemg18b  40851  ltrnco  40891  tendocan  40996  cdlemk28-3  41080  cdlemk11t  41118  dia2dimlem6  41241  dia2dimlem12  41247  dihlsscpre  41406  dihord4  41430  dihord5b  41431  dihmeetlem3N  41477  dihmeetlem20N  41498  dvh4dimlem  41615  lclkrlem2y  41703  mapdpglem24  41876  mapdpglem32  41877  mapdpg  41878  baerlem3lem2  41882  baerlem5alem2  41883  baerlem5blem2  41884  mapdh9a  41961  mapdh9aOLDN  41962  hdmap14lem6  42045  hdmapglem7  42101  indstrd  42359  nnadddir  42440  nnmulcom  42442  sn-addlid  42574  remulcand  42609  mzpexpmpt  42902  pellexlem5  42990  pellex  42992  pell14qrexpclnn0  43023  pellfundex  43043  monotuz  43098  monotoddzzfi  43099  rmxypos  43104  jm2.17a  43117  jm2.17b  43118  rmygeid  43121  jm2.19lem3  43148  jm2.15nn0  43160  jm2.16nn0  43161  aomclem2  43212  aomclem6  43216  dfac11  43219  hbtlem5  43285  cnsrexpcl  43322  cantnf2  43482  dflim5  43486  relexpxpnnidm  43860  relexpiidm  43861  relexpss1d  43862  iunrelexpmin1  43865  relexpmulnn  43866  iunrelexpmin2  43869  relexp01min  43870  relexp0a  43873  relexpxpmin  43874  relexpaddss  43875  trclimalb2  43883  tfindsd  44367  3impexpbicomi  44638  ee333  44664  eel12131  44869  eel2122old  44874  e333  44889  ordelordALTVD  45023  refsumcn  45191  uzwo4  45214  ssinc  45247  ssdec  45248  iunincfi  45254  restuni3  45278  eliuniin2  45280  rabssd  45302  reximdd  45308  suprnmpt  45334  disjf1o  45351  disjinfi  45352  ssnnf1octb  45354  choicefi  45360  mapssbi  45373  unirnmapsn  45374  iunmapsn  45377  rnmptlb  45403  rnmptbddlem  45404  infnsuprnmpt  45410  fperiodmullem  45467  upbdrech  45469  ssfiunibd  45473  supxrgere  45494  iuneqfzuzlem  45495  supxrgelem  45498  supxrge  45499  suplesup  45500  infrpge  45512  infleinf  45532  suplesup2  45536  supxrunb3  45559  infleinf2  45574  rexabslelem  45578  infrnmptle  45583  infxrunb3rnmpt  45588  iccshift  45680  iooshift  45684  fmul01  45742  fmuldfeq  45745  fmul01lt1  45748  mullimc  45778  islptre  45781  mullimcf  45785  limcperiod  45790  islpcn  45799  limsupre  45801  limcleqr  45804  neglimc  45807  addlimc  45808  0ellimcdiv  45809  limclner  45811  fnlimfvre  45834  limsuppnflem  45870  limsupmnfuzlem  45886  limsupre3lem  45892  limsupre3uzlem  45895  climuzlem  45903  limsupgtlem  45937  coskpi2  46026  cosknegpi  46029  cncfshift  46034  cncfperiod  46039  icccncfext  46047  dvnmptdivc  46098  dvnmptconst  46101  dvnmul  46103  dvmptfprodlem  46104  dvmptfprod  46105  dvnprodlem1  46106  dvnprodlem2  46107  iblspltprt  46133  itgspltprt  46139  itgperiod  46141  ismbl3  46146  stoweidlem3  46163  stoweidlem31  46191  stoweidlem59  46219  stirlinglem13  46246  fourierdlem41  46308  fourierdlem42  46309  fourierdlem48  46314  fourierdlem51  46317  fourierdlem70  46336  fourierdlem71  46337  fourierdlem73  46339  fourierdlem80  46346  fourierdlem81  46347  fourierdlem89  46355  fourierdlem91  46357  fourierdlem93  46359  fourierdlem97  46363  elaa2  46394  qndenserrnopnlem  46457  salexct  46494  subsaliuncl  46518  subsalsal  46519  sge0tsms  46540  sge0f1o  46542  sge0fsum  46547  sge0supre  46549  sge0sup  46551  sge0rnbnd  46553  sge0gerp  46555  sge0pnffigt  46556  sge0lefi  46558  sge0ltfirp  46560  sge0resrn  46564  sge0resplit  46566  sge0split  46569  sge0iunmptlemfi  46573  sge0iunmptlemre  46575  sge0iunmpt  46578  sge0rpcpnf  46581  sge0isum  46587  sge0xp  46589  sge0xaddlem2  46594  sge0uzfsumgt  46604  sge0seq  46606  sge0reuz  46607  nnfoctbdjlem  46615  nnfoctbdj  46616  iundjiun  46620  meadjiunlem  46625  voliunsge0lem  46632  meaiuninclem  46640  meaiininc2  46648  carageniuncllem1  46681  carageniuncllem2  46682  caratheodorylem1  46686  caratheodorylem2  46687  isomenndlem  46690  ovnsupge0  46717  ovnlerp  46722  ovncvrrp  46724  ovnsubaddlem1  46730  hoidmvval0  46747  hoidmv1lelem3  46753  hoidmv1le  46754  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  ovnhoilem2  46762  opnvonmbllem2  46793  ovnovollem3  46818  vonioo  46842  vonicc  46845  pimiooltgt  46870  sssmf  46898  smfaddlem1  46923  smflimlem6  46936  smfmullem4  46954  smfpimbor1lem1  46958  smfco  46962  smfpimcc  46968  smflimmpt  46970  smfinflem  46977  smflimsuplem7  46986  smflimsuplem8  46987  smflimsupmpt  46989  smfliminfmpt  46992  cfsetsnfsetf1  47221  2tceilhalfelfzo1  47494  elsetpreimafveqfv  47554  iccpartiltu  47584  sprsymrelfvlem  47652  reuopreuprim  47688  goldbachth  47709  fmtnofac1  47732  prmdvdsfmtnof1lem1  47746  lighneal  47773  grimuhgr  48049  uhgrimedgi  48052  uhgrimisgrgriclem  48092  clnbgrgrim  48096  grimedg  48097  usgrgrtrirex  48112  isubgr3stgrlem3  48130  isubgr3stgrlem6  48133  uspgrlimlem2  48151  grlimgrtri  48165  grlicsym  48175  clnbgr3stgrgrlic  48182  gpgusgralem  48218  gpgedgvtx1  48224  gpgvtxedg0  48225  gpgvtxedg1  48226  uspgropssxp  48306  rngccatidALTV  48434  ringccatidALTV  48468  lcosslsp  48600  fllog2  48730  dignn0flhalf  48780  fv1arycl  48799  1arymaptf1  48804  fv2arycl  48810  2arymaptf1  48815  itschlc0yqe  48922  itsclc0xyqsol  48930  seposep  49087  iscnrm3lem6  49099  iunord  49837  setrec2fun  49853