Theorem 3exp 1137

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expb  1138  3expib  1140  3com12  1141  3com13  1142  pm3.2an3  1359  3exp1  1371  3expd  1372  exp5o  1374  3ecase  1505  rexlimdv3a  3172  rabssdv  4029  reupick2  4284  disjiund  5102  otiunsndisj  5505  wefrc  5657  tz7.7  6390  unizlim  6489  funimassd  6951  fvelimad  6952  fveqdmss  7077  fompt  7117  f1resrcmplf1d  7278  f1oiso2  7359  ssorduni  7784  tfisi  7861  resf1extb  7937  funeldmdif  8051  poxp  8130  poseq  8160  fpr3g  8288  frrlem10  8298  smo11  8357  tfrlem5  8372  odi  8570  omass  8571  nndi  8615  nnmass  8616  naddoa  8695  undifixp  8938  findcard  9155  php3  9200  ac6sfi  9251  domunfican  9288  mapfien2  9376  fisup2g  9436  fiinf2g  9469  ttrclss  9696  ttrclselem2  9702  indcardi  10041  acndom  10051  ackbij1lem16  10233  infpssrlem4  10305  fin23lem11  10316  isfin2-2  10318  fin23lem34  10345  fin1a2lem10  10408  hsmexlem2  10426  axcc3  10437  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  axcclem  10456  ttukeyg  10516  axdclem2  10519  axacndlem4  10610  axacndlem5  10611  axacnd  10612  tskr1om2  10768  tskwe2  10773  tskord  10780  tskcard  10781  tskuni  10783  tskwun  10784  gruiin  10810  grudomon  10817  gruina  10818  mulcanpi  10900  adderpq  10956  mulerpq  10957  dedekindle  11389  divgt0  12098  divge0  12099  nnne0  12285  nnadddir  12307  nnmulcom  12309  uzind  12704  uzind2  12705  iccsplit  13528  ssnn0fi  14039  expmordi  14221  sqlecan  14263  modexp  14292  expnngt1  14295  facavg  14355  2cshwcshw  14886  relexpcnv  15096  relexpaddnn  15112  relexpaddg  15114  pwdif  15945  prodfn0  15971  prodfrec  15972  ntrivcvgfvn0  15976  fprodabs  16051  bpolycl  16128  bpolydif  16131  fprodefsum  16171  dvdsmodexp  16340  dvdsaddre2b  16387  nn0rppwr  16641  dvdsnprmd  16770  2mulprm  16773  prmndvdsfaclt  16806  ncoprmlnprm  16809  fermltl  16865  pceu  16928  setsstruct2  17256  setsstruct  17258  mreexexd  17726  isglbd  18587  symgpssefmnd  19510  pmtrfrn  19572  psgnunilem4  19611  ablsimpgprmd  20231  mulgass2  20438  islss4  21133  lspsneu  21297  lspfixed  21302  lspexch  21303  lsmcv  21315  lspsolvlem  21316  rnglidlmcl  21391  unichnlidl  21412  xrsdsreclblem  21613  nzerooringczr  21680  isphld  21854  mdetralt  22815  mdetunilem9  22827  fiinopn  23108  neips  23320  tpnei  23328  neindisj2  23330  opnneiid  23333  hausnei2  23560  cmpsublem  23606  cmpsub  23607  cmpcld  23609  comppfsc  23740  filufint  24128  cfinufil  24136  rnelfm  24161  alexsubALTlem1  24255  alexsubALTlem4  24258  alexsubALT  24259  tsmsxp  24363  neibl  24709  tngngp3  24864  tgqioo  25008  ovolunlem2  25708  iunmbl2  25767  itg1le  25923  vieta1  26524  aannenlem2  26543  aalioulem3  26548  aalioulem4  26549  aaliou2  26554  wilthlem3  27285  bcmono  27492  gausslemma2dlem1a  27580  sltstr  28031  sltsun1  28032  sltsun2  28033  ltslpss  28152  precsexlem8  28458  precsexlem9  28459  precsex  28462  onsfi  28600  oldfib  28621  expscllem  28674  expsgt0  28681  pw2cut  28704  pw2cut2  28706  bdaypw2n0bnd  28708  bdayfin  28731  iscgrglt  28834  axcontlem7  29375  elntg2  29390  edglnl  29548  numedglnl  29549  lfuhgr2  29554  ausgrumgri  29575  ausgrusgri  29576  usgrausgrb  29577  usgredg2vtxeuALT  29630  ushgredgedg  29637  ushgredgedgloop  29639  nbuhgr2vtx1edgb  29760  cusgrsize2inds  29861  upgrewlkle2  30014  wlkl1loop  30045  redwlk  30078  pthdivtx  30139  pthdadjvtx  30140  upgr2pthnlp  30145  upgrspthswlk  30151  clwlkl1loop  30197  cyclnumvtx  30215  wwlksnred  30308  wwlksnextbi  30310  elwwlks2ons3im  30370  usgrwwlks2on  30374  umgrwwlks2on  30375  clwwlknwwlksn  30456  clwwlkinwwlk  30458  wwlksext2clwwlk  30475  1pthon2v  30575  uhgr3cyclex  30604  n4cyclfrgr  30713  frgrwopreg  30745  numclwwlk1lem2f1  30779  clwwlknonclwlknonf1o  30784  wlkl0  30789  frgrreggt1  30815  frgrreg  30816  frgrregord013  30817  chintcli  31754  spansnss  31994  elspansn4  31996  chscllem4  32063  hoadddir  32227  adjmul  32515  kbass6  32544  spansncv2  32716  sumdmdii  32838  nexple  33247  bnj1417  35494  cusgredgex  35664  sat1el2xp  35908  fmlasuc  35915  satffunlem1lem1  35931  satffunlem2lem1  35933  mclsind  36099  iprodefisumlem  36269  btwndiff  36556  elicc3  36885  finminlem  36886  axtcond  37046  ttcmin  37064  sdclem2  38451  clmgmOLD  38560  grpomndo  38584  zerdivemp1x  38656  lsmsat  39840  lsmcv2  39861  lcvat  39862  lsatcveq0  39864  lcvexchlem4  39869  lcvexchlem5  39870  islshpcv  39885  l1cvpat  39886  lshpkrlem6  39947  omlfh3N  40091  cvlsupr4  40177  cvlsupr5  40178  cvlsupr6  40179  2llnneN  40241  hlrelat3  40244  cvrval3  40245  cvrval4N  40246  cvrexchlem  40251  2atlt  40271  cvrat4  40275  atbtwnexOLDN  40279  atbtwnex  40280  athgt  40288  3dim1  40299  3dim2  40300  3dim3  40301  1cvratex  40305  llnle  40350  atcvrlln2  40351  atcvrlln  40352  2llnmat  40356  lplnle  40372  lplnnle2at  40373  lplnnlelln  40375  llncvrlpln2  40389  2llnjN  40399  lvoli2  40413  lvolnlelln  40416  lvolnlelpln  40417  4atlem10  40438  4atlem11  40441  4atlem12  40444  lplncvrlvol2  40447  2lplnj  40452  lneq2at  40610  lnatexN  40611  lnjatN  40612  lncvrat  40614  2lnat  40616  cdlemb  40626  paddasslem14  40665  llnexchb2  40701  dalawlem10  40712  dalawlem13  40715  dalawlem14  40716  dalaw  40718  pclclN  40723  pclfinN  40732  osumcllem11N  40798  lhp2lt  40833  lhpexle3lem  40843  4atexlem7  40907  ldilcnv  40947  ldilco  40948  ltrncnv  40978  trlval2  40995  cdleme24  41184  cdleme26ee  41192  cdleme28  41205  cdleme32le  41279  cdleme50trn2  41383  cdleme50ltrn  41389  cdleme  41392  cdlemf1  41393  cdlemf  41395  cdlemg1cex  41420  cdlemg2ce  41424  cdlemg18b  41511  ltrnco  41551  tendocan  41656  cdlemk28-3  41740  cdlemk11t  41778  dia2dimlem6  41901  dia2dimlem12  41907  dihlsscpre  42066  dihord4  42090  dihord5b  42091  dihmeetlem3N  42137  dihmeetlem20N  42158  dvh4dimlem  42275  lclkrlem2y  42363  mapdpglem24  42536  mapdpglem32  42537  mapdpg  42538  baerlem3lem2  42542  baerlem5alem2  42543  baerlem5blem2  42544  mapdh9a  42621  mapdh9aOLDN  42622  hdmap14lem6  42705  hdmapglem7  42761  indstrd  43018  sn-addlid  43223  remulcand  43258  mzpexpmpt  43534  pellexlem5  43618  pellex  43620  pell14qrexpclnn0  43651  pellfundex  43671  monotuz  43726  monotoddzzfi  43727  rmxypos  43732  jm2.17a  43745  jm2.17b  43746  rmygeid  43749  jm2.19lem3  43776  jm2.15nn0  43788  jm2.16nn0  43789  aomclem2  43840  aomclem6  43844  dfac11  43847  hbtlem5  43913  cnsrexpcl  43950  cantnf2  44110  dflim5  44114  relexpxpnnidm  44487  relexpiidm  44488  relexpss1d  44489  iunrelexpmin1  44492  relexpmulnn  44493  iunrelexpmin2  44496  relexp01min  44497  relexp0a  44500  relexpxpmin  44501  relexpaddss  44502  trclimalb2  44510  tfindsd  44992  3impexpbicomi  45248  ee333  45274  eel12131  45479  eel2122old  45484  e333  45499  ordelordALTVD  45633  refsumcn  45808  uzwo4  45831  ssinc  45863  ssdec  45864  iunincfi  45870  restuni3  45894  eliuniin2  45896  rabssd  45918  reximdd  45924  suprnmpt  45950  disjf1o  45967  disjinfi  45968  ssnnf1octb  45970  choicefi  45975  mapssbi  45987  unirnmapsn  45988  iunmapsn  45991  rnmptlb  46016  rnmptbddlem  46017  infnsuprnmpt  46023  fperiodmullem  46080  upbdrech  46082  ssfiunibd  46086  supxrgere  46107  iuneqfzuzlem  46108  supxrgelem  46111  supxrge  46112  suplesup  46113  infrpge  46125  infleinf  46145  suplesup2  46149  supxrunb3  46172  infleinf2  46186  rexabslelem  46190  infrnmptle  46195  infxrunb3rnmpt  46200  iccshift  46292  iooshift  46296  fmul01  46354  fmuldfeq  46357  fmul01lt1  46360  mullimc  46390  islptre  46393  mullimcf  46397  limcperiod  46402  islpcn  46411  limsupre  46413  limcleqr  46416  neglimc  46419  addlimc  46420  0ellimcdiv  46421  limclner  46423  fnlimfvre  46446  limsuppnflem  46482  limsupmnfuzlem  46498  limsupre3lem  46504  limsupre3uzlem  46507  climuzlem  46515  limsupgtlem  46549  coskpi2  46638  cosknegpi  46641  cncfshift  46646  cncfperiod  46651  icccncfext  46659  dvnmptdivc  46710  dvnmptconst  46713  dvnmul  46715  dvmptfprodlem  46716  dvmptfprod  46717  dvnprodlem1  46718  dvnprodlem2  46719  iblspltprt  46745  itgspltprt  46751  itgperiod  46753  ismbl3  46758  stoweidlem3  46775  stoweidlem31  46803  stoweidlem59  46831  stirlinglem13  46858  fourierdlem41  46920  fourierdlem42  46921  fourierdlem48  46926  fourierdlem51  46929  fourierdlem70  46948  fourierdlem71  46949  fourierdlem73  46951  fourierdlem80  46958  fourierdlem81  46959  fourierdlem89  46967  fourierdlem91  46969  fourierdlem93  46971  fourierdlem97  46975  elaa2  47006  qndenserrnopnlem  47069  salexct  47106  subsaliuncl  47130  subsalsal  47131  sge0tsms  47152  sge0f1o  47154  sge0fsum  47159  sge0supre  47161  sge0sup  47163  sge0rnbnd  47165  sge0gerp  47167  sge0pnffigt  47168  sge0lefi  47170  sge0ltfirp  47172  sge0resrn  47176  sge0resplit  47178  sge0split  47181  sge0iunmptlemfi  47185  sge0iunmptlemre  47187  sge0iunmpt  47190  sge0rpcpnf  47193  sge0isum  47199  sge0xp  47201  sge0xaddlem2  47206  sge0uzfsumgt  47216  sge0seq  47218  sge0reuz  47219  nnfoctbdjlem  47227  nnfoctbdj  47228  iundjiun  47232  meadjiunlem  47237  voliunsge0lem  47244  meaiuninclem  47252  meaiininc2  47260  carageniuncllem1  47293  carageniuncllem2  47294  caratheodorylem1  47298  caratheodorylem2  47299  isomenndlem  47302  ovnsupge0  47329  ovnlerp  47334  ovncvrrp  47336  ovnsubaddlem1  47342  hoidmvval0  47359  hoidmv1lelem3  47365  hoidmv1le  47366  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem3  47369  ovnhoilem2  47374  opnvonmbllem2  47405  ovnovollem3  47430  vonioo  47454  vonicc  47457  pimiooltgt  47482  smfaddlem1  47535  smflimlem6  47548  smfmullem4  47566  smfpimbor1lem1  47570  smfco  47574  smfpimcc  47580  smflimmpt  47582  smfinflem  47589  smflimsuplem7  47598  smflimsuplem8  47599  smflimsupmpt  47601  smfliminfmpt  47604  cfsetsnfsetf1  47854  nnmul2b  48126  2tceilhalfelfzo1  48131  elsetpreimafveqfv  48199  iccpartiltu  48229  sprsymrelfvlem  48297  reuopreuprim  48333  nprmmul2  48335  goldbachth  48357  fmtnofac1  48380  prmdvdsfmtnof1lem1  48394  lighneal  48421  grimuhgr  48710  uhgrimedgi  48713  uhgrimisgrgriclem  48753  clnbgrgrim  48757  grimedg  48758  usgrgrtrirex  48773  isubgr3stgrlem3  48791  isubgr3stgrlem6  48794  uspgrlimlem2  48812  grlimgrtri  48826  grlicsym  48836  clnbgr3stgrgrlic  48843  gpgusgralem  48879  gpgedgvtx1  48885  gpgvtxedg0  48886  gpgvtxedg1  48887  uspgropssxp  48967  rngccatidALTV  49094  ringccatidALTV  49128  lcosslsp  49275  fllog2  49405  dignn0flhalf  49455  fv1arycl  49474  1arymaptf1  49479  fv2arycl  49485  2arymaptf1  49490  itschlc0yqe  49597  itsclc0xyqsol  49605  seposep  49761  iscnrm3lem6  49773  iunord  50511  setrec2fun  50527