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  3167  rabssdv  3998  reupick2  4275  disjiund  5093  otiunsndisj  5493  wefrc  5645  tz7.7  6391  unizlim  6490  funimassd  6956  fvelimad  6957  fveqdmss  7083  fompt  7123  f1resrcmplf1d  7283  f1oiso2  7364  ssorduni  7797  tfisi  7874  resf1extb  7950  funeldmdif  8064  poxp  8147  poseq  8182  fpr3g  8311  frrlem10  8321  smo11  8380  tfrlem5  8395  odi  8595  omass  8596  nndi  8640  nnmass  8641  naddoa  8720  undifixp  8970  findcard  9187  php3  9232  ac6sfi  9283  domunfican  9321  mapfien2  9408  fisup2g  9468  fiinf2g  9501  ttrclss  9728  ttrclselem2  9734  setrec2fun  9980  indcardi  10127  acndom  10137  ackbij1lem16  10319  infpssrlem4  10391  fin23lem11  10402  isfin2-2  10404  fin23lem34  10431  fin1a2lem10  10494  hsmexlem2  10512  axcc3  10523  domtriomlem  10527  axdc3lem2  10536  axdc3lem4  10538  axcclem  10542  ttukeyg  10602  axdclem2  10605  axacndlem4  10702  axacndlem5  10703  axacnd  10704  tskhf  10860  tskwe2  10865  tskord  10872  tskcard  10873  tskuni  10875  tskwun  10876  gruiin  10902  grudomon  10909  gruina  10910  mulcanpi  10992  adderpq  11048  mulerpq  11049  dedekindle  11481  divgt0  12192  divge0  12193  nnne0  12379  nnadddir  12401  nnmulcom  12403  uzind  12798  uzind2  12799  iccsplit  13623  ssnn0fi  14135  expmordi  14317  sqlecan  14360  modexp  14389  expnngt1  14392  facavg  14452  2cshwcshw  14984  relexpcnv  15197  relexpaddnn  15213  relexpaddg  15215  pwdif  16046  prodfn0  16072  prodfrec  16073  ntrivcvgfvn0  16077  fprodabs  16150  bpolycl  16227  bpolydif  16230  fprodefsum  16270  dvdsmodexp  16439  dvdsaddre2b  16486  nn0rppwr  16744  dvdsnprmd  16874  2mulprm  16877  prmndvdsfaclt  16910  ncoprmlnprm  16913  fermltl  16970  pceu  17033  setsstruct2  17361  setsstruct  17363  mreexexd  17831  isglbd  18692  symgpssefmnd  19619  pmtrfrn  19681  psgnunilem4  19720  ablsimpgprmd  20340  mulgass2  20549  islss4  21246  lspsneu  21410  lspfixed  21415  lspexch  21416  lsmcv  21428  lspsolvlem  21429  rnglidlmcl  21504  unichnlidl  21525  xrsdsreclblem  21728  nzerooringczr  21795  isphld  21969  mdetralt  22932  mdetunilem9  22944  fiinopn  23228  neips  23440  tpnei  23448  neindisj2  23450  opnneiid  23453  hausnei2  23680  cmpsublem  23726  cmpsub  23727  cmpcld  23729  comppfsc  23860  filufint  24248  cfinufil  24256  rnelfm  24281  alexsubALTlem1  24375  alexsubALTlem4  24378  alexsubALT  24379  tsmsxp  24483  neibl  24829  tngngp3  24984  tgqioo  25128  ovolunlem2  25828  iunmbl2  25887  itg1le  26043  vieta1  26644  aannenlem2  26665  aalioulem3  26670  aalioulem4  26671  aaliou2  26676  wilthlem3  27406  bcmono  27613  gausslemma2dlem1a  27701  sltstr  28182  sltsun1  28183  sltsun2  28184  ltslpss  28303  precsexlem8  28609  precsexlem9  28610  precsex  28613  onsfi  28751  oldfib  28772  expscllem  28825  expsgt0  28832  pw2cut  28855  pw2cut2  28857  bdaypw2n0bnd  28859  bdayfin  28882  iscgrglt  28986  axcontlem7  29557  elntg2  29572  edglnl  29730  numedglnl  29731  lfuhgr2  29736  ausgrumgri  29757  ausgrusgri  29758  usgrausgrb  29759  usgredg2vtxeuALT  29812  ushgredgedg  29819  ushgredgedgloop  29821  nbuhgr2vtx1edgb  29942  cusgrsize2inds  30043  upgrewlkle2  30196  wlkl1loop  30227  redwlk  30260  pthdivtx  30321  pthdadjvtx  30322  upgr2pthnlp  30327  upgrspthswlk  30333  clwlkl1loop  30379  cyclnumvtx  30397  wwlksnred  30490  wwlksnextbi  30492  elwwlks2ons3im  30552  usgrwwlks2on  30556  umgrwwlks2on  30557  clwwlknwwlksn  30638  clwwlkinwwlk  30640  wwlksext2clwwlk  30657  1pthon2v  30763  uhgr3cyclex  30792  n4cyclfrgr  30901  frgrwopreg  30933  numclwwlk1lem2f1  30967  clwwlknonclwlknonf1o  30972  wlkl0  30977  frgrreggt1  31003  frgrreg  31004  frgrregord013  31005  chintcli  31942  spansnss  32182  elspansn4  32184  chscllem4  32251  hoadddir  32415  adjmul  32703  kbass6  32732  spansncv2  32904  sumdmdii  33026  nexple  33474  bnj1417  35721  cusgredgex  36014  sat1el2xp  36262  fmlasuc  36269  satffunlem1lem1  36285  satffunlem2lem1  36287  mclsind  36453  iprodefisumlem  36629  btwndiff  36916  elicc3  37229  finminlem  37230  axtcond  37390  ttcmin  37408  sdclem2  38813  clmgmOLD  38922  grpomndo  38946  zerdivemp1x  39018  lsmsat  40202  lsmcv2  40223  lcvat  40224  lsatcveq0  40226  lcvexchlem4  40231  lcvexchlem5  40232  islshpcv  40247  l1cvpat  40248  lshpkrlem6  40309  omlfh3N  40453  cvlsupr4  40539  cvlsupr5  40540  cvlsupr6  40541  2llnneN  40603  hlrelat3  40606  cvrval3  40607  cvrval4N  40608  cvrexchlem  40613  2atlt  40633  cvrat4  40637  atbtwnexOLDN  40641  atbtwnex  40642  athgt  40650  3dim1  40661  3dim2  40662  3dim3  40663  1cvratex  40667  llnle  40712  atcvrlln2  40713  atcvrlln  40714  2llnmat  40718  lplnle  40734  lplnnle2at  40735  lplnnlelln  40737  llncvrlpln2  40751  2llnjN  40761  lvoli2  40775  lvolnlelln  40778  lvolnlelpln  40779  4atlem10  40800  4atlem11  40803  4atlem12  40806  lplncvrlvol2  40809  2lplnj  40814  lneq2at  40972  lnatexN  40973  lnjatN  40974  lncvrat  40976  2lnat  40978  cdlemb  40988  paddasslem14  41027  llnexchb2  41063  dalawlem10  41074  dalawlem13  41077  dalawlem14  41078  dalaw  41080  pclclN  41085  pclfinN  41094  osumcllem11N  41160  lhp2lt  41195  lhpexle3lem  41205  4atexlem7  41269  ldilcnv  41309  ldilco  41310  ltrncnv  41340  trlval2  41357  cdleme24  41546  cdleme26ee  41554  cdleme28  41567  cdleme32le  41641  cdleme50trn2  41745  cdleme50ltrn  41751  cdleme  41754  cdlemf1  41755  cdlemf  41757  cdlemg1cex  41782  cdlemg2ce  41786  cdlemg18b  41873  ltrnco  41913  tendocan  42018  cdlemk28-3  42102  cdlemk11t  42140  dia2dimlem6  42263  dia2dimlem12  42269  dihlsscpre  42428  dihord4  42452  dihord5b  42453  dihmeetlem3N  42499  dihmeetlem20N  42520  dvh4dimlem  42637  lclkrlem2y  42725  mapdpglem24  42898  mapdpglem32  42899  mapdpg  42900  baerlem3lem2  42904  baerlem5alem2  42905  baerlem5blem2  42906  mapdh9a  42983  mapdh9aOLDN  42984  hdmap14lem6  43067  hdmapglem7  43123  indstrd  43380  sn-addlid  43592  remulcand  43627  mzpexpmpt  43893  pellexlem5  43977  pellex  43979  pell14qrexpclnn0  44010  pellfundex  44030  monotuz  44085  monotoddzzfi  44086  rmxypos  44091  jm2.17a  44104  jm2.17b  44105  rmygeid  44108  jm2.19lem3  44135  jm2.15nn0  44147  jm2.16nn0  44148  aomclem2  44194  aomclem6  44198  dfac11  44201  hbtlem5  44267  cnsrexpcl  44304  cantnf2  44464  dflim5  44468  relexpxpnnidm  44840  relexpiidm  44841  relexpss1d  44842  iunrelexpmin1  44845  relexpmulnn  44846  iunrelexpmin2  44849  relexp01min  44850  relexp0a  44853  relexpxpmin  44854  relexpaddss  44855  trclimalb2  44863  tfindsd  45345  3impexpbicomi  45600  ee333  45626  eel12131  45831  eel2122old  45836  e333  45851  ordelordALTVD  45985  refsumcn  46183  uzwo4  46206  ssinc  46238  ssdec  46239  iunincfi  46245  restuni3  46269  eliuniin2  46271  rabssd  46293  reximdd  46299  suprnmpt  46325  disjf1o  46342  disjinfi  46343  ssnnf1octb  46345  choicefi  46350  mapssbi  46362  unirnmapsn  46363  iunmapsn  46366  rnmptlb  46391  rnmptbddlem  46392  infnsuprnmpt  46398  fperiodmullem  46455  upbdrech  46457  ssfiunibd  46461  supxrgere  46481  iuneqfzuzlem  46482  supxrgelem  46485  supxrge  46486  suplesup  46487  infrpge  46499  infleinf  46519  suplesup2  46523  supxrunb3  46546  infleinf2  46560  rexabslelem  46564  infrnmptle  46569  infxrunb3rnmpt  46574  iccshift  46666  iooshift  46670  fmul01  46728  fmuldfeq  46731  fmul01lt1  46734  mullimc  46764  islptre  46767  mullimcf  46771  limcperiod  46776  islpcn  46785  limsupre  46787  limcleqr  46790  neglimc  46793  addlimc  46794  0ellimcdiv  46795  limclner  46797  fnlimfvre  46820  limsuppnflem  46856  limsupmnfuzlem  46872  limsupre3lem  46878  limsupre3uzlem  46881  climuzlem  46889  limsupgtlem  46923  coskpi2  47012  cosknegpi  47015  cncfshift  47020  cncfperiod  47025  icccncfext  47033  dvnmptdivc  47084  dvnmptconst  47087  dvnmul  47089  dvmptfprodlem  47090  dvmptfprod  47091  dvnprodlem1  47092  dvnprodlem2  47093  iblspltprt  47119  itgspltprt  47125  itgperiod  47127  ismbl3  47132  stoweidlem3  47149  stoweidlem31  47177  stoweidlem59  47205  stirlinglem13  47232  fourierdlem41  47294  fourierdlem42  47295  fourierdlem48  47300  fourierdlem51  47303  fourierdlem70  47322  fourierdlem71  47323  fourierdlem73  47325  fourierdlem80  47332  fourierdlem81  47333  fourierdlem89  47341  fourierdlem91  47343  fourierdlem93  47345  fourierdlem97  47349  elaa2  47380  qndenserrnopnlem  47443  salexct  47480  subsaliuncl  47504  subsalsal  47505  sge0tsms  47526  sge0f1o  47528  sge0fsum  47533  sge0supre  47535  sge0sup  47537  sge0rnbnd  47539  sge0gerp  47541  sge0pnffigt  47542  sge0lefi  47544  sge0ltfirp  47546  sge0resrn  47550  sge0resplit  47552  sge0split  47555  sge0iunmptlemfi  47559  sge0iunmptlemre  47561  sge0iunmpt  47564  sge0rpcpnf  47567  sge0isum  47573  sge0xp  47575  sge0xaddlem2  47580  sge0uzfsumgt  47590  sge0seq  47592  sge0reuz  47593  nnfoctbdjlem  47601  nnfoctbdj  47602  iundjiun  47606  meadjiunlem  47611  voliunsge0lem  47618  meaiuninclem  47626  meaiininc2  47634  carageniuncllem1  47667  carageniuncllem2  47668  caratheodorylem1  47672  caratheodorylem2  47673  isomenndlem  47676  ovnsupge0  47703  ovnlerp  47708  ovncvrrp  47710  ovnsubaddlem1  47716  hoidmvval0  47733  hoidmv1lelem3  47739  hoidmv1le  47740  hoidmvlelem1  47741  hoidmvlelem2  47742  hoidmvlelem3  47743  ovnhoilem2  47748  opnvonmbllem2  47779  ovnovollem3  47804  vonioo  47828  vonicc  47831  pimiooltgt  47856  smfaddlem1  47909  smflimlem6  47922  smfmullem4  47940  smfpimbor1lem1  47944  smfco  47948  smfpimcc  47954  smflimmpt  47956  smfinflem  47963  smflimsuplem7  47972  smflimsuplem8  47973  smflimsupmpt  47975  smfliminfmpt  47978  cfsetsnfsetf1  48265  nnmul2b  48537  2tceilhalfelfzo1  48542  elsetpreimafveqfv  48610  iccpartiltu  48640  sprsymrelfvlem  48708  reuopreuprim  48744  nprmmul2  48746  goldbachth  48768  fmtnofac1  48791  prmdvdsfmtnof1lem1  48805  lighneal  48832  grimuhgr  49121  uhgrimedgi  49124  uhgrimisgrgriclem  49164  clnbgrgrim  49168  grimedg  49169  usgrgrtrirex  49184  isubgr3stgrlem3  49202  isubgr3stgrlem6  49205  uspgrlimlem2  49223  grlimgrtri  49237  grlicsym  49247  clnbgr3stgrgrlic  49254  gpgusgralem  49290  gpgedgvtx1  49296  gpgvtxedg0  49297  gpgvtxedg1  49298  uspgropssxp  49378  rngccatidALTV  49505  ringccatidALTV  49539  lcosslsp  49686  fllog2  49816  dignn0flhalf  49866  fv1arycl  49885  1arymaptf1  49890  fv2arycl  49896  2arymaptf1  49901  itschlc0yqe  50008  itsclc0xyqsol  50016  seposep  50176  iscnrm3lem6  50188  iunord  50995