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  3139  rabssdv  4041  reupick2  4297  disjiund  5101  otiunsndisj  5483  wefrc  5635  tz7.7  6361  unizlim  6460  funimassd  6930  fvelimad  6931  fveqdmss  7053  fompt  7093  f1oiso2  7330  ssorduni  7758  sucexeloniOLD  7789  tfisi  7838  resf1extb  7913  funeldmdif  8030  poxp  8110  poseq  8140  fpr3g  8267  frrlem10  8277  smo11  8336  tfrlem5  8351  odi  8546  omass  8547  nndi  8590  nnmass  8591  naddoa  8669  undifixp  8910  findcard  9133  php3  9179  ac6sfi  9238  domunfican  9279  mapfien2  9367  fisup2g  9427  fiinf2g  9460  ttrclss  9680  ttrclselem2  9686  indcardi  10001  acndom  10011  ackbij1lem16  10194  infpssrlem4  10266  fin23lem11  10277  isfin2-2  10279  fin23lem34  10306  fin1a2lem10  10369  hsmexlem2  10387  axcc3  10398  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axcclem  10417  ttukeyg  10477  axdclem2  10480  axacndlem4  10570  axacndlem5  10571  axacnd  10572  tskr1om2  10728  tskwe2  10733  tskord  10740  tskcard  10741  tskuni  10743  tskwun  10744  gruiin  10770  grudomon  10777  gruina  10778  mulcanpi  10860  adderpq  10916  mulerpq  10917  dedekindle  11345  divgt0  12058  divge0  12059  nnne0  12227  uzind  12633  uzind2  12634  iccsplit  13453  ssnn0fi  13957  expmordi  14139  sqlecan  14181  modexp  14210  expnngt1  14213  facavg  14273  2cshwcshw  14798  relexpcnv  15008  relexpaddnn  15024  relexpaddg  15026  pwdif  15841  prodfn0  15867  prodfrec  15868  ntrivcvgfvn0  15872  fprodabs  15947  bpolycl  16025  bpolydif  16028  fprodefsum  16068  dvdsmodexp  16237  dvdsaddre2b  16284  nn0rppwr  16538  dvdsnprmd  16667  2mulprm  16670  prmndvdsfaclt  16702  ncoprmlnprm  16705  fermltl  16761  pceu  16824  setsstruct2  17151  setsstruct  17153  mreexexd  17616  isglbd  18475  symgpssefmnd  19333  pmtrfrn  19395  psgnunilem4  19434  ablsimpgprmd  20054  mulgass2  20225  islss4  20875  lspsneu  21040  lspfixed  21045  lspexch  21046  lsmcv  21058  lspsolvlem  21059  rnglidlmcl  21133  xrsdsreclblem  21336  nzerooringczr  21397  isphld  21570  mdetralt  22502  mdetunilem9  22514  fiinopn  22795  neips  23007  tpnei  23015  neindisj2  23017  opnneiid  23020  hausnei2  23247  cmpsublem  23293  cmpsub  23294  cmpcld  23296  comppfsc  23426  filufint  23814  cfinufil  23822  rnelfm  23847  alexsubALTlem1  23941  alexsubALTlem4  23944  alexsubALT  23945  tsmsxp  24049  neibl  24396  tngngp3  24551  tgqioo  24695  ovolunlem2  25406  iunmbl2  25465  itg1le  25621  vieta1  26227  aannenlem2  26244  aalioulem3  26249  aalioulem4  26250  aaliou2  26255  wilthlem3  26987  bcmono  27195  gausslemma2dlem1a  27283  sslttr  27726  ssltun1  27727  ssltun2  27728  sltlpss  27826  precsexlem8  28123  precsexlem9  28124  precsex  28127  onsfi  28254  expscllem  28323  expsgt0  28329  pw2cut  28342  iscgrglt  28448  axcontlem7  28904  elntg2  28919  edglnl  29077  numedglnl  29078  ausgrumgri  29101  ausgrusgri  29102  usgrausgrb  29103  usgredg2vtxeuALT  29156  ushgredgedg  29163  ushgredgedgloop  29165  nbuhgr2vtx1edgb  29286  cusgrsize2inds  29388  upgrewlkle2  29541  wlkl1loop  29573  redwlk  29607  pthdivtx  29664  pthdadjvtx  29665  upgr2pthnlp  29669  upgrspthswlk  29675  clwlkl1loop  29720  cyclnumvtx  29737  wwlksnred  29829  wwlksnextbi  29831  elwwlks2ons3im  29891  umgrwwlks2on  29894  clwwlknwwlksn  29974  clwwlkinwwlk  29976  wwlksext2clwwlk  29993  1pthon2v  30089  uhgr3cyclex  30118  n4cyclfrgr  30227  frgrwopreg  30259  numclwwlk1lem2f1  30293  clwwlknonclwlknonf1o  30298  wlkl0  30303  frgrreggt1  30329  frgrreg  30330  frgrregord013  30331  chintcli  31267  spansnss  31507  elspansn4  31509  chscllem4  31576  hoadddir  31740  adjmul  32028  kbass6  32057  spansncv2  32229  sumdmdii  32351  nexple  32776  bnj1417  35038  lfuhgr2  35113  cusgredgex  35116  sat1el2xp  35373  fmlasuc  35380  satffunlem1lem1  35396  satffunlem2lem1  35398  mclsind  35564  iprodefisumlem  35734  btwndiff  36022  elicc3  36312  finminlem  36313  sdclem2  37743  clmgmOLD  37852  grpomndo  37876  zerdivemp1x  37948  lsmsat  39008  lsmcv2  39029  lcvat  39030  lsatcveq0  39032  lcvexchlem4  39037  lcvexchlem5  39038  islshpcv  39053  l1cvpat  39054  lshpkrlem6  39115  omlfh3N  39259  cvlsupr4  39345  cvlsupr5  39346  cvlsupr6  39347  2llnneN  39410  hlrelat3  39413  cvrval3  39414  cvrval4N  39415  cvrexchlem  39420  2atlt  39440  cvrat4  39444  atbtwnexOLDN  39448  atbtwnex  39449  athgt  39457  3dim1  39468  3dim2  39469  3dim3  39470  1cvratex  39474  llnle  39519  atcvrlln2  39520  atcvrlln  39521  2llnmat  39525  lplnle  39541  lplnnle2at  39542  lplnnlelln  39544  llncvrlpln2  39558  2llnjN  39568  lvoli2  39582  lvolnlelln  39585  lvolnlelpln  39586  4atlem10  39607  4atlem11  39610  4atlem12  39613  lplncvrlvol2  39616  2lplnj  39621  lneq2at  39779  lnatexN  39780  lnjatN  39781  lncvrat  39783  2lnat  39785  cdlemb  39795  paddasslem14  39834  llnexchb2  39870  dalawlem10  39881  dalawlem13  39884  dalawlem14  39885  dalaw  39887  pclclN  39892  pclfinN  39901  osumcllem11N  39967  lhp2lt  40002  lhpexle3lem  40012  4atexlem7  40076  ldilcnv  40116  ldilco  40117  ltrncnv  40147  trlval2  40164  cdleme24  40353  cdleme26ee  40361  cdleme28  40374  cdleme32le  40448  cdleme50trn2  40552  cdleme50ltrn  40558  cdleme  40561  cdlemf1  40562  cdlemf  40564  cdlemg1cex  40589  cdlemg2ce  40593  cdlemg18b  40680  ltrnco  40720  tendocan  40825  cdlemk28-3  40909  cdlemk11t  40947  dia2dimlem6  41070  dia2dimlem12  41076  dihlsscpre  41235  dihord4  41259  dihord5b  41260  dihmeetlem3N  41306  dihmeetlem20N  41327  dvh4dimlem  41444  lclkrlem2y  41532  mapdpglem24  41705  mapdpglem32  41706  mapdpg  41707  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  mapdh9a  41790  mapdh9aOLDN  41791  hdmap14lem6  41874  hdmapglem7  41930  indstrd  42188  nnadddir  42265  nnmulcom  42267  sn-addlid  42399  remulcand  42434  mzpexpmpt  42740  pellexlem5  42828  pellex  42830  pell14qrexpclnn0  42861  pellfundex  42881  monotuz  42937  monotoddzzfi  42938  rmxypos  42943  jm2.17a  42956  jm2.17b  42957  rmygeid  42960  jm2.19lem3  42987  jm2.15nn0  42999  jm2.16nn0  43000  aomclem2  43051  aomclem6  43055  dfac11  43058  hbtlem5  43124  cnsrexpcl  43161  cantnf2  43321  dflim5  43325  relexpxpnnidm  43699  relexpiidm  43700  relexpss1d  43701  iunrelexpmin1  43704  relexpmulnn  43705  iunrelexpmin2  43708  relexp01min  43709  relexp0a  43712  relexpxpmin  43713  relexpaddss  43714  trclimalb2  43722  tfindsd  44206  3impexpbicomi  44478  ee333  44504  eel12131  44709  eel2122old  44714  e333  44729  ordelordALTVD  44863  refsumcn  45031  uzwo4  45054  ssinc  45088  ssdec  45089  iunincfi  45095  restuni3  45119  eliuniin2  45121  rabssd  45143  reximdd  45149  suprnmpt  45175  disjf1o  45192  disjinfi  45193  ssnnf1octb  45195  choicefi  45201  mapssbi  45214  unirnmapsn  45215  iunmapsn  45218  rnmptlb  45244  rnmptbddlem  45245  infnsuprnmpt  45251  fperiodmullem  45308  upbdrech  45310  ssfiunibd  45314  supxrgere  45336  iuneqfzuzlem  45337  supxrgelem  45340  supxrge  45341  suplesup  45342  infrpge  45354  infleinf  45375  suplesup2  45379  supxrunb3  45402  infleinf2  45417  rexabslelem  45421  infrnmptle  45426  infxrunb3rnmpt  45431  iccshift  45523  iooshift  45527  fmul01  45585  fmuldfeq  45588  fmul01lt1  45591  mullimc  45621  islptre  45624  mullimcf  45628  limcperiod  45633  islpcn  45644  limsupre  45646  limcleqr  45649  neglimc  45652  addlimc  45653  0ellimcdiv  45654  limclner  45656  fnlimfvre  45679  limsuppnflem  45715  limsupmnfuzlem  45731  limsupre3lem  45737  limsupre3uzlem  45740  climuzlem  45748  limsupgtlem  45782  coskpi2  45871  cosknegpi  45874  cncfshift  45879  cncfperiod  45884  icccncfext  45892  dvnmptdivc  45943  dvnmptconst  45946  dvnmul  45948  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  iblspltprt  45978  itgspltprt  45984  itgperiod  45986  ismbl3  45991  stoweidlem3  46008  stoweidlem31  46036  stoweidlem59  46064  stirlinglem13  46091  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem51  46162  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem80  46191  fourierdlem81  46192  fourierdlem89  46200  fourierdlem91  46202  fourierdlem93  46204  fourierdlem97  46208  elaa2  46239  qndenserrnopnlem  46302  salexct  46339  subsaliuncl  46363  subsalsal  46364  sge0tsms  46385  sge0f1o  46387  sge0fsum  46392  sge0supre  46394  sge0sup  46396  sge0rnbnd  46398  sge0gerp  46400  sge0pnffigt  46401  sge0lefi  46403  sge0ltfirp  46405  sge0resrn  46409  sge0resplit  46411  sge0split  46414  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0rpcpnf  46426  sge0isum  46432  sge0xp  46434  sge0xaddlem2  46439  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  nnfoctbdjlem  46460  nnfoctbdj  46461  iundjiun  46465  meadjiunlem  46470  voliunsge0lem  46477  meaiuninclem  46485  meaiininc2  46493  carageniuncllem1  46526  carageniuncllem2  46527  caratheodorylem1  46531  caratheodorylem2  46532  isomenndlem  46535  ovnsupge0  46562  ovnlerp  46567  ovncvrrp  46569  ovnsubaddlem1  46575  hoidmvval0  46592  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem2  46607  opnvonmbllem2  46638  ovnovollem3  46663  vonioo  46687  vonicc  46690  pimiooltgt  46715  sssmf  46743  smfaddlem1  46768  smflimlem6  46781  smfmullem4  46799  smfpimbor1lem1  46803  smfco  46807  smfpimcc  46813  smflimmpt  46815  smfinflem  46822  smflimsuplem7  46831  smflimsuplem8  46832  smflimsupmpt  46834  smfliminfmpt  46837  cfsetsnfsetf1  47064  2tceilhalfelfzo1  47337  elsetpreimafveqfv  47397  iccpartiltu  47427  sprsymrelfvlem  47495  reuopreuprim  47531  goldbachth  47552  fmtnofac1  47575  prmdvdsfmtnof1lem1  47589  lighneal  47616  grimuhgr  47891  uhgrimedgi  47894  uhgrimisgrgriclem  47934  clnbgrgrim  47938  grimedg  47939  usgrgrtrirex  47953  isubgr3stgrlem3  47971  isubgr3stgrlem6  47974  uspgrlimlem2  47992  grlimgrtri  47999  grlicsym  48009  clnbgr3stgrgrlic  48015  gpgusgralem  48051  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  uspgropssxp  48136  rngccatidALTV  48264  ringccatidALTV  48298  lcosslsp  48431  fllog2  48561  dignn0flhalf  48611  fv1arycl  48630  1arymaptf1  48635  fv2arycl  48641  2arymaptf1  48646  itschlc0yqe  48753  itsclc0xyqsol  48761  seposep  48918  iscnrm3lem6  48930  iunord  49669  setrec2fun  49685