Theorem 3exp 1116

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3expb  1117  3expib  1119  3com12  1120  3com13  1121  pm3.2an3  1337  3exp1  1349  3expd  1350  exp5o  1352  3ecase  1470  rexlimdv3a  3155  rabssdv  4070  reupick2  4322  disjiund  5140  otiunsndisj  5524  wefrc  5674  tz7.7  6398  unizlim  6495  funimassd  6968  fvelimad  6969  fveqdmss  7091  fompt  7131  f1oiso2  7364  ssorduni  7785  sucexeloniOLD  7817  suceloniOLD  7819  tfisi  7867  funeldmdif  8056  poxp  8137  poseq  8167  fpr3g  8295  frrlem10  8305  smo11  8389  tfrlem5  8405  odi  8604  omass  8605  nndi  8648  nnmass  8649  undifixp  8957  findcard  9192  php3  9241  ac6sfi  9316  domunfican  9350  mapfien2  9438  fisup2g  9497  fiinf2g  9529  ttrclss  9749  ttrclselem2  9755  indcardi  10070  acndom  10080  ackbij1lem16  10264  infpssrlem4  10335  fin23lem11  10346  isfin2-2  10348  fin23lem34  10375  fin1a2lem10  10438  hsmexlem2  10456  axcc3  10467  domtriomlem  10471  axdc3lem2  10480  axdc3lem4  10482  axcclem  10486  ttukeyg  10546  axdclem2  10549  axacndlem4  10639  axacndlem5  10640  axacnd  10641  tskr1om2  10797  tskwe2  10802  tskord  10809  tskcard  10810  tskuni  10812  tskwun  10813  gruiin  10839  grudomon  10846  gruina  10847  mulcanpi  10929  adderpq  10985  mulerpq  10986  dedekindle  11414  divgt0  12118  divge0  12119  nnne0  12282  uzind  12690  uzind2  12691  iccsplit  13500  ssnn0fi  13988  expmordi  14169  sqlecan  14210  modexp  14238  expnngt1  14241  facavg  14298  2cshwcshw  14814  relexpcnv  15020  relexpaddnn  15036  relexpaddg  15038  pwdif  15852  prodfn0  15878  prodfrec  15879  ntrivcvgfvn0  15883  fprodabs  15956  bpolycl  16034  bpolydif  16037  fprodefsum  16077  dvdsmodexp  16244  dvdsaddre2b  16289  dvdsnprmd  16666  2mulprm  16669  prmndvdsfaclt  16702  ncoprmlnprm  16705  fermltl  16758  pceu  16820  setsstruct2  17148  setsstruct  17150  mreexexd  17633  isglbd  18506  symgpssefmnd  19355  pmtrfrn  19418  psgnunilem4  19457  ablsimpgprmd  20077  mulgass2  20250  islss4  20851  lspsneu  21016  lspfixed  21021  lspexch  21022  lsmcv  21034  lspsolvlem  21035  rnglidlmcl  21117  xrsdsreclblem  21350  nzerooringczr  21411  isphld  21591  mdetralt  22528  mdetunilem9  22540  fiinopn  22821  neips  23035  tpnei  23043  neindisj2  23045  opnneiid  23048  hausnei2  23275  cmpsublem  23321  cmpsub  23322  cmpcld  23324  comppfsc  23454  filufint  23842  cfinufil  23850  rnelfm  23875  alexsubALTlem1  23969  alexsubALTlem4  23972  alexsubALT  23973  tsmsxp  24077  neibl  24428  tngngp3  24591  tgqioo  24734  ovolunlem2  25445  iunmbl2  25504  itg1le  25661  vieta1  26265  aannenlem2  26282  aalioulem3  26287  aalioulem4  26288  aaliou2  26293  wilthlem3  27020  bcmono  27228  gausslemma2dlem1a  27316  sslttr  27758  ssltun1  27759  ssltun2  27760  sltlpss  27851  precsexlem8  28130  precsexlem9  28131  precsex  28134  iscgrglt  28336  axcontlem7  28799  elntg2  28814  edglnl  28974  numedglnl  28975  ausgrumgri  28998  ausgrusgri  28999  usgrausgrb  29000  usgredg2vtxeuALT  29053  ushgredgedg  29060  ushgredgedgloop  29062  nbuhgr2vtx1edgb  29183  cusgrsize2inds  29285  upgrewlkle2  29438  wlkl1loop  29470  redwlk  29504  pthdivtx  29561  pthdadjvtx  29562  upgr2pthnlp  29564  upgrspthswlk  29570  clwlkl1loop  29615  wwlksnred  29721  wwlksnextbi  29723  elwwlks2ons3im  29783  umgrwwlks2on  29786  clwwlknwwlksn  29866  clwwlkinwwlk  29868  wwlksext2clwwlk  29885  1pthon2v  29981  uhgr3cyclex  30010  n4cyclfrgr  30119  frgrwopreg  30151  numclwwlk1lem2f1  30185  clwwlknonclwlknonf1o  30190  wlkl0  30195  frgrreggt1  30221  frgrreg  30222  frgrregord013  30223  chintcli  31159  spansnss  31399  elspansn4  31401  chscllem4  31468  hoadddir  31632  adjmul  31920  kbass6  31949  spansncv2  32121  sumdmdii  32243  nexple  33633  bnj1417  34677  lfuhgr2  34733  cusgredgex  34736  sat1el2xp  34994  fmlasuc  35001  satffunlem1lem1  35017  satffunlem2lem1  35019  mclsind  35185  iprodefisumlem  35339  btwndiff  35628  elicc3  35806  finminlem  35807  sdclem2  37220  clmgmOLD  37329  grpomndo  37353  zerdivemp1x  37425  lsmsat  38484  lsmcv2  38505  lcvat  38506  lsatcveq0  38508  lcvexchlem4  38513  lcvexchlem5  38514  islshpcv  38529  l1cvpat  38530  lshpkrlem6  38591  omlfh3N  38735  cvlsupr4  38821  cvlsupr5  38822  cvlsupr6  38823  2llnneN  38886  hlrelat3  38889  cvrval3  38890  cvrval4N  38891  cvrexchlem  38896  2atlt  38916  cvrat4  38920  atbtwnexOLDN  38924  atbtwnex  38925  athgt  38933  3dim1  38944  3dim2  38945  3dim3  38946  1cvratex  38950  llnle  38995  atcvrlln2  38996  atcvrlln  38997  2llnmat  39001  lplnle  39017  lplnnle2at  39018  lplnnlelln  39020  llncvrlpln2  39034  2llnjN  39044  lvoli2  39058  lvolnlelln  39061  lvolnlelpln  39062  4atlem10  39083  4atlem11  39086  4atlem12  39089  lplncvrlvol2  39092  2lplnj  39097  lneq2at  39255  lnatexN  39256  lnjatN  39257  lncvrat  39259  2lnat  39261  cdlemb  39271  paddasslem14  39310  llnexchb2  39346  dalawlem10  39357  dalawlem13  39360  dalawlem14  39361  dalaw  39363  pclclN  39368  pclfinN  39377  osumcllem11N  39443  lhp2lt  39478  lhpexle3lem  39488  4atexlem7  39552  ldilcnv  39592  ldilco  39593  ltrncnv  39623  trlval2  39640  cdleme24  39829  cdleme26ee  39837  cdleme28  39850  cdleme32le  39924  cdleme50trn2  40028  cdleme50ltrn  40034  cdleme  40037  cdlemf1  40038  cdlemf  40040  cdlemg1cex  40065  cdlemg2ce  40069  cdlemg18b  40156  ltrnco  40196  tendocan  40301  cdlemk28-3  40385  cdlemk11t  40423  dia2dimlem6  40546  dia2dimlem12  40552  dihlsscpre  40711  dihord4  40735  dihord5b  40736  dihmeetlem3N  40782  dihmeetlem20N  40803  dvh4dimlem  40920  lclkrlem2y  41008  mapdpglem24  41181  mapdpglem32  41182  mapdpg  41183  baerlem3lem2  41187  baerlem5alem2  41188  baerlem5blem2  41189  mapdh9a  41266  mapdh9aOLDN  41267  hdmap14lem6  41350  hdmapglem7  41406  nnadddir  41848  nnmulcom  41850  nn0rppwr  41896  sn-addlid  41962  remulcand  41996  mzpexpmpt  42168  pellexlem5  42256  pellex  42258  pell14qrexpclnn0  42289  pellfundex  42309  monotuz  42365  monotoddzzfi  42366  rmxypos  42371  jm2.17a  42384  jm2.17b  42385  rmygeid  42388  jm2.19lem3  42415  jm2.15nn0  42427  jm2.16nn0  42428  aomclem2  42482  aomclem6  42486  dfac11  42489  hbtlem5  42555  cnsrexpcl  42592  cantnf2  42757  dflim5  42761  relexpxpnnidm  43136  relexpiidm  43137  relexpss1d  43138  iunrelexpmin1  43141  relexpmulnn  43142  iunrelexpmin2  43145  relexp01min  43146  relexp0a  43149  relexpxpmin  43150  relexpaddss  43151  trclimalb2  43159  tfindsd  43645  3impexpbicomi  43922  ee333  43949  eel12131  44155  eel2122old  44160  e333  44175  ordelordALTVD  44309  refsumcn  44395  uzwo4  44420  ssinc  44456  ssdec  44457  iunincfi  44463  restuni3  44487  eliuniin2  44489  rabssd  44511  reximdd  44521  suprnmpt  44550  disjf1o  44567  disjinfi  44568  ssnnf1octb  44570  choicefi  44576  mapssbi  44589  unirnmapsn  44590  ssmapsn  44592  iunmapsn  44593  rnmptlb  44621  rnmptbddlem  44622  infnsuprnmpt  44628  fperiodmullem  44687  upbdrech  44689  ssfiunibd  44693  supxrgere  44717  iuneqfzuzlem  44718  supxrgelem  44721  supxrge  44722  suplesup  44723  infrpge  44735  infleinf  44756  suplesup2  44760  supxrunb3  44783  infleinf2  44798  rexabslelem  44802  infrnmptle  44807  infxrunb3rnmpt  44812  iccshift  44905  iooshift  44909  fmul01  44970  fmuldfeq  44973  fmul01lt1  44976  mullimc  45006  islptre  45009  mullimcf  45013  limcperiod  45018  islpcn  45029  limsupre  45031  limcleqr  45034  neglimc  45037  addlimc  45038  0ellimcdiv  45039  limclner  45041  fnlimfvre  45064  limsuppnflem  45100  limsupmnfuzlem  45116  limsupre3lem  45122  limsupre3uzlem  45125  climuzlem  45133  limsupgtlem  45167  coskpi2  45256  cosknegpi  45259  cncfshift  45264  cncfperiod  45269  icccncfext  45277  dvnmptdivc  45328  dvnmptconst  45331  dvnmul  45333  dvmptfprodlem  45334  dvmptfprod  45335  dvnprodlem1  45336  dvnprodlem2  45337  iblspltprt  45363  itgspltprt  45369  itgperiod  45371  ismbl3  45376  stoweidlem3  45393  stoweidlem31  45421  stoweidlem59  45449  stirlinglem13  45476  fourierdlem41  45538  fourierdlem42  45539  fourierdlem48  45544  fourierdlem51  45547  fourierdlem70  45566  fourierdlem71  45567  fourierdlem73  45569  fourierdlem80  45576  fourierdlem81  45577  fourierdlem89  45585  fourierdlem91  45587  fourierdlem93  45589  fourierdlem97  45593  elaa2  45624  qndenserrnopnlem  45687  salexct  45724  subsaliuncl  45748  subsalsal  45749  sge0tsms  45770  sge0f1o  45772  sge0fsum  45777  sge0supre  45779  sge0sup  45781  sge0rnbnd  45783  sge0gerp  45785  sge0pnffigt  45786  sge0lefi  45788  sge0ltfirp  45790  sge0resrn  45794  sge0resplit  45796  sge0split  45799  sge0iunmptlemfi  45803  sge0iunmptlemre  45805  sge0iunmpt  45808  sge0rpcpnf  45811  sge0isum  45817  sge0xp  45819  sge0xaddlem2  45824  sge0uzfsumgt  45834  sge0seq  45836  sge0reuz  45837  nnfoctbdjlem  45845  nnfoctbdj  45846  iundjiun  45850  meadjiunlem  45855  voliunsge0lem  45862  meaiuninclem  45870  meaiininc2  45878  carageniuncllem1  45911  carageniuncllem2  45912  caratheodorylem1  45916  caratheodorylem2  45917  isomenndlem  45920  ovnsupge0  45947  ovnlerp  45952  ovncvrrp  45954  ovnsubaddlem1  45960  hoidmvval0  45977  hoidmv1lelem3  45983  hoidmv1le  45984  hoidmvlelem1  45985  hoidmvlelem2  45986  hoidmvlelem3  45987  ovnhoilem2  45992  opnvonmbllem2  46023  ovnovollem3  46048  vonioo  46072  vonicc  46075  pimiooltgt  46100  sssmf  46128  smfaddlem1  46153  smflimlem6  46166  smfmullem4  46184  smfpimbor1lem1  46188  smfco  46192  smfpimcc  46198  smflimmpt  46200  smfinflem  46207  smflimsuplem7  46216  smflimsuplem8  46217  smflimsupmpt  46219  smfliminfmpt  46222  cfsetsnfsetf1  46443  elsetpreimafveqfv  46734  iccpartiltu  46764  sprsymrelfvlem  46832  reuopreuprim  46868  goldbachth  46889  fmtnofac1  46912  prmdvdsfmtnof1lem1  46926  lighneal  46953  grimuhgr  47227  uspgropssxp  47257  rngccatidALTV  47385  ringccatidALTV  47419  lcosslsp  47557  fllog2  47692  dignn0flhalf  47742  fv1arycl  47761  1arymaptf1  47766  fv2arycl  47772  2arymaptf1  47777  itschlc0yqe  47884  itsclc0xyqsol  47892  seposep  47995  iscnrm3lem6  48008  iunord  48158  setrec2fun  48174