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  1506  rexlimdv3a  3171  rabssdv  4002  reupick2  4279  disjiund  5099  otiunsndisj  5500  wefrc  5652  tz7.7  6414  unizlim  6513  funimassd  6982  fvelimad  6983  fveqdmss  7110  fompt  7150  f1resrcmplf1d  7310  f1oiso2  7391  ssorduni  7827  tfisi  7904  resf1extb  7980  funeldmdif  8094  poxp  8177  poseq  8212  fpr3g  8341  frrlem10  8351  smo11  8410  tfrlem5  8425  odi  8625  omass  8626  nndi  8670  nnmass  8671  naddoa  8750  undifixp  9000  findcard  9217  php3  9262  ac6sfi  9313  domunfican  9351  mapfien2  9438  fisup2g  9498  fiinf2g  9531  ttrclss  9758  ttrclselem2  9764  setrec2fun  10010  indcardi  10159  acndom  10169  ackbij1lem16  10351  infpssrlem4  10423  fin23lem11  10434  isfin2-2  10436  fin23lem34  10463  fin1a2lem10  10526  hsmexlem2  10544  axcc3  10555  domtriomlem  10559  axdc3lem2  10568  axdc3lem4  10570  axcclem  10574  ttukeyg  10634  axdclem2  10637  axacndlem4  10734  axacndlem5  10735  axacnd  10736  tskhf  10892  tskwe2  10897  tskord  10904  tskcard  10905  tskuni  10907  tskwun  10908  gruiin  10934  grudomon  10941  gruina  10942  mulcanpi  11024  adderpq  11080  mulerpq  11081  dedekindle  11513  divgt0  12225  divge0  12226  nnne0  12412  nnadddir  12434  nnmulcom  12436  uzind  12831  uzind2  12832  iccsplit  13656  ssnn0fi  14168  expmordi  14350  sqlecan  14393  modexp  14423  expnngt1  14426  facavg  14486  2cshwcshw  15018  relexpcnv  15231  relexpaddnn  15247  relexpaddg  15249  pwdif  16081  prodfn0  16107  prodfrec  16108  ntrivcvgfvn0  16112  fprodabs  16185  bpolycl  16262  bpolydif  16265  fprodefsum  16305  dvdsmodexp  16474  dvdsaddre2b  16521  nn0rppwr  16779  dvdsnprmd  16909  2mulprm  16912  prmndvdsfaclt  16945  ncoprmlnprm  16948  fermltl  17005  pceu  17068  setsstruct2  17396  setsstruct  17398  mreexexd  17872  isglbd  18733  symgpssefmnd  19661  pmtrfrn  19723  psgnunilem4  19762  ablsimpgprmd  20382  mulgass2  20591  islss4  21288  lspsneu  21452  lspfixed  21457  lspexch  21458  lsmcv  21470  lspsolvlem  21471  rnglidlmcl  21546  unichnlidl  21567  xrsdsreclblem  21771  cnsrexpcl  21778  nzerooringczr  21841  isphld  22015  mdetralt  22978  mdetunilem9  22990  fiinopn  23274  neips  23486  tpnei  23494  neindisj2  23496  opnneiid  23499  hausnei2  23726  cmpsublem  23772  cmpsub  23773  cmpcld  23775  comppfsc  23906  filufint  24294  cfinufil  24302  rnelfm  24327  alexsubALTlem1  24421  alexsubALTlem4  24424  alexsubALT  24425  tsmsxp  24529  neibl  24875  tngngp3  25030  tgqioo  25174  ovolunlem2  25874  iunmbl2  25933  itg1le  26089  vieta1  26690  aannenlem2  26713  aalioulem3  26718  aalioulem4  26719  aaliou2  26724  wilthlem3  27454  bcmono  27661  gausslemma2dlem1a  27749  sltstr  28230  sltsun1  28231  sltsun2  28232  ltslpss  28351  precsexlem8  28657  precsexlem9  28658  precsex  28661  onsfi  28799  oldfib  28820  expscllem  28873  expsgt0  28880  pw2cut  28903  pw2cut2  28905  bdaypw2n0bnd  28907  bdayfin  28930  iscgrglt  29034  axcontlem7  29605  elntg2  29620  edglnl  29778  numedglnl  29779  lfuhgr2  29784  ausgrumgri  29805  ausgrusgri  29806  usgrausgrb  29807  usgredg2vtxeuALT  29860  ushgredgedg  29867  ushgredgedgloop  29869  nbuhgr2vtx1edgb  29990  cusgrsize2inds  30091  upgrewlkle2  30244  wlkl1loop  30275  redwlk  30308  pthdivtx  30369  pthdadjvtx  30370  upgr2pthnlp  30375  upgrspthswlk  30381  clwlkl1loop  30427  cyclnumvtx  30445  wwlksnred  30538  wwlksnextbi  30540  elwwlks2ons3im  30600  usgrwwlks2on  30604  umgrwwlks2on  30605  clwwlknwwlksn  30686  clwwlkinwwlk  30688  wwlksext2clwwlk  30705  1pthon2v  30811  uhgr3cyclex  30840  n4cyclfrgr  30949  frgrwopreg  30981  numclwwlk1lem2f1  31015  clwwlknonclwlknonf1o  31020  wlkl0  31025  frgrreggt1  31051  frgrreg  31052  frgrregord013  31053  chintcli  31990  spansnss  32230  elspansn4  32232  chscllem4  32299  hoadddir  32463  adjmul  32751  kbass6  32780  spansncv2  32952  sumdmdii  33074  nexple  33520  bnj1417  35782  cusgredgex  36104  sat1el2xp  36352  fmlasuc  36359  satffunlem1lem1  36375  satffunlem2lem1  36377  mclsind  36543  iprodefisumlem  36720  btwndiff  37007  elicc3  37320  finminlem  37321  axtcond  37481  ttcmin  37499  sdclem2  38942  clmgmOLD  39051  grpomndo  39075  zerdivemp1x  39147  lsmsat  40331  lsmcv2  40352  lcvat  40353  lsatcveq0  40355  lcvexchlem4  40360  lcvexchlem5  40361  islshpcv  40376  l1cvpat  40377  lshpkrlem6  40438  omlfh3N  40582  cvlsupr4  40668  cvlsupr5  40669  cvlsupr6  40670  2llnneN  40732  hlrelat3  40735  cvrval3  40736  cvrval4N  40737  cvrexchlem  40742  2atlt  40762  cvrat4  40766  atbtwnexOLDN  40770  atbtwnex  40771  athgt  40779  3dim1  40790  3dim2  40791  3dim3  40792  1cvratex  40796  llnle  40841  atcvrlln2  40842  atcvrlln  40843  2llnmat  40847  lplnle  40863  lplnnle2at  40864  lplnnlelln  40866  llncvrlpln2  40880  2llnjN  40890  lvoli2  40904  lvolnlelln  40907  lvolnlelpln  40908  4atlem10  40929  4atlem11  40932  4atlem12  40935  lplncvrlvol2  40938  2lplnj  40943  lneq2at  41101  lnatexN  41102  lnjatN  41103  lncvrat  41105  2lnat  41107  cdlemb  41117  paddasslem14  41156  llnexchb2  41192  dalawlem10  41203  dalawlem13  41206  dalawlem14  41207  dalaw  41209  pclclN  41214  pclfinN  41223  osumcllem11N  41289  lhp2lt  41324  lhpexle3lem  41334  4atexlem7  41398  ldilcnv  41438  ldilco  41439  ltrncnv  41469  trlval2  41486  cdleme24  41675  cdleme26ee  41683  cdleme28  41696  cdleme32le  41770  cdleme50trn2  41874  cdleme50ltrn  41880  cdleme  41883  cdlemf1  41884  cdlemf  41886  cdlemg1cex  41911  cdlemg2ce  41915  cdlemg18b  42002  ltrnco  42042  tendocan  42147  cdlemk28-3  42231  cdlemk11t  42269  dia2dimlem6  42392  dia2dimlem12  42398  dihlsscpre  42557  dihord4  42581  dihord5b  42582  dihmeetlem3N  42628  dihmeetlem20N  42649  dvh4dimlem  42766  lclkrlem2y  42854  mapdpglem24  43027  mapdpglem32  43028  mapdpg  43029  baerlem3lem2  43033  baerlem5alem2  43034  baerlem5blem2  43035  mapdh9a  43112  mapdh9aOLDN  43113  hdmap14lem6  43196  hdmapglem7  43252  indstrd  43509  sn-addlid  43721  remulcand  43756  mzpexpmpt  44022  pellexlem5  44106  pellex  44108  pell14qrexpclnn0  44139  pellfundex  44159  monotuz  44214  monotoddzzfi  44215  rmxypos  44220  jm2.17a  44233  jm2.17b  44234  rmygeid  44237  jm2.19lem3  44264  jm2.15nn0  44276  jm2.16nn0  44277  aomclem2  44323  aomclem6  44327  dfac11  44330  hbtlem5  44395  cantnf2  44588  dflim5  44592  relexpxpnnidm  44964  relexpiidm  44965  relexpss1d  44966  iunrelexpmin1  44969  relexpmulnn  44970  iunrelexpmin2  44973  relexp01min  44974  relexp0a  44977  relexpxpmin  44978  relexpaddss  44979  trclimalb2  44987  tfindsd  45469  3impexpbicomi  45724  ee333  45750  eel12131  45955  eel2122old  45960  e333  45975  ordelordALTVD  46109  refsumcn  46321  uzwo4  46344  ssinc  46375  ssdec  46376  iunincfi  46382  restuni3  46406  eliuniin2  46408  rabssd  46430  reximdd  46436  suprnmpt  46462  disjf1o  46479  disjinfi  46480  ssnnf1octb  46482  choicefi  46487  mapssbi  46499  unirnmapsn  46500  iunmapsn  46503  rnmptlb  46528  rnmptbddlem  46529  infnsuprnmpt  46535  fperiodmullem  46592  upbdrech  46594  ssfiunibd  46598  supxrgere  46618  iuneqfzuzlem  46619  supxrgelem  46622  supxrge  46623  suplesup  46624  infrpge  46636  infleinf  46656  suplesup2  46660  supxrunb3  46683  infleinf2  46697  rexabslelem  46701  infrnmptle  46706  infxrunb3rnmpt  46711  iccshift  46803  iooshift  46807  fmul01  46865  fmuldfeq  46868  fmul01lt1  46871  mullimc  46901  islptre  46904  mullimcf  46908  limcperiod  46913  islpcn  46922  limsupre  46924  limcleqr  46927  neglimc  46930  addlimc  46931  0ellimcdiv  46932  limclner  46934  fnlimfvre  46957  limsuppnflem  46993  limsupmnfuzlem  47009  limsupre3lem  47015  limsupre3uzlem  47018  climuzlem  47026  limsupgtlem  47060  coskpi2  47149  cosknegpi  47152  cncfshift  47157  cncfperiod  47162  icccncfext  47170  dvnmptdivc  47221  dvnmptconst  47224  dvnmul  47226  dvmptfprodlem  47227  dvmptfprod  47228  dvnprodlem1  47229  dvnprodlem2  47230  iblspltprt  47256  itgspltprt  47262  itgperiod  47264  ismbl3  47269  stoweidlem3  47286  stoweidlem31  47314  stoweidlem59  47342  stirlinglem13  47369  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem51  47440  fourierdlem70  47459  fourierdlem71  47460  fourierdlem73  47462  fourierdlem80  47469  fourierdlem81  47470  fourierdlem89  47478  fourierdlem91  47480  fourierdlem93  47482  fourierdlem97  47486  elaa2  47517  qndenserrnopnlem  47580  salexct  47617  subsaliuncl  47641  subsalsal  47642  sge0tsms  47663  sge0f1o  47665  sge0fsum  47670  sge0supre  47672  sge0sup  47674  sge0rnbnd  47676  sge0gerp  47678  sge0pnffigt  47679  sge0lefi  47681  sge0ltfirp  47683  sge0resrn  47687  sge0resplit  47689  sge0split  47692  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0rpcpnf  47704  sge0isum  47710  sge0xp  47712  sge0xaddlem2  47717  sge0uzfsumgt  47727  sge0seq  47729  sge0reuz  47730  nnfoctbdjlem  47738  nnfoctbdj  47739  iundjiun  47743  meadjiunlem  47748  voliunsge0lem  47755  meaiuninclem  47763  meaiininc2  47771  carageniuncllem1  47804  carageniuncllem2  47805  caratheodorylem1  47809  caratheodorylem2  47810  isomenndlem  47813  ovnsupge0  47840  ovnlerp  47845  ovncvrrp  47847  ovnsubaddlem1  47853  hoidmvval0  47870  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  ovnhoilem2  47885  opnvonmbllem2  47916  ovnovollem3  47941  vonioo  47965  vonicc  47968  pimiooltgt  47993  smfaddlem1  48046  smflimlem6  48059  smfmullem4  48077  smfpimbor1lem1  48081  smfco  48085  smfpimcc  48091  smflimmpt  48093  smfinflem  48100  smflimsuplem7  48109  smflimsuplem8  48110  smflimsupmpt  48112  smfliminfmpt  48115  cfsetsnfsetf1  48402  nnmul2b  48674  2tceilhalfelfzo1  48679  elsetpreimafveqfv  48747  iccpartiltu  48777  sprsymrelfvlem  48845  reuopreuprim  48881  nprmmul2  48883  goldbachth  48905  fmtnofac1  48928  prmdvdsfmtnof1lem1  48942  lighneal  48969  grimuhgr  49258  uhgrimedgi  49261  uhgrimisgrgriclem  49301  clnbgrgrim  49305  grimedg  49306  usgrgrtrirex  49321  isubgr3stgrlem3  49339  isubgr3stgrlem6  49342  uspgrlimlem2  49360  grlimgrtri  49374  grlicsym  49384  clnbgr3stgrgrlic  49391  gpgusgralem  49427  gpgedgvtx1  49433  gpgvtxedg0  49434  gpgvtxedg1  49435  uspgropssxp  49515  rngccatidALTV  49642  ringccatidALTV  49676  lcosslsp  49881  fllog2  50011  dignn0flhalf  50061  fv1arycl  50080  1arymaptf1  50085  fv2arycl  50091  2arymaptf1  50096  itschlc0yqe  50203  itsclc0xyqsol  50211  seposep  50371  iscnrm3lem6  50383  iunord  51190