MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp Structured version   Visualization version   GIF version

Theorem 3exp 1113
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
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1112 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32exp31 420 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  3expb  1114  3expib  1116  3com12  1117  3com13  1118  pm3.2an3  1334  3exp1  1346  3expd  1347  exp5o  1349  3ecase  1467  rexlimdv3a  3291  rabssdv  4055  reupick2  4293  disjiund  5053  otiunsndisj  5407  wefrc  5548  predpo  6164  tz7.7  6215  unizlim  6305  fvelimad  6729  fveqdmss  6842  f1oiso2  7097  ssorduni  7488  suceloni  7516  tfisi  7561  funeldmdif  7738  poxp  7813  smo11  7992  tfrlem5  8007  odi  8195  omass  8196  nndi  8239  nnmass  8240  undifixp  8487  findcard  8746  ac6sfi  8751  domunfican  8780  mapfien2  8861  fisup2g  8921  fiinf2g  8953  indcardi  9456  acndom  9466  ackbij1lem16  9646  infpssrlem4  9717  fin23lem11  9728  isfin2-2  9730  fin23lem34  9757  fin1a2lem10  9820  hsmexlem2  9838  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axcclem  9868  ttukeyg  9928  axdclem2  9931  axacndlem4  10021  axacndlem5  10022  axacnd  10023  tskr1om2  10179  tskwe2  10184  tskord  10191  tskcard  10192  tskuni  10194  tskwun  10195  gruiin  10221  grudomon  10228  gruina  10229  mulcanpi  10311  adderpq  10367  mulerpq  10368  dedekindle  10793  divgt0  11497  divge0  11498  nnne0  11660  uzind  12063  uzind2  12064  iccsplit  12861  ssnn0fi  13343  expmordi  13521  sqlecan  13561  modexp  13589  expnngt1  13592  facavg  13651  2cshwcshw  14177  relexpcnv  14384  relexpreld  14389  relexpaddnn  14400  relexpaddg  14402  pwdif  15213  prodfn0  15240  prodfrec  15241  ntrivcvgfvn0  15245  fprodabs  15318  bpolycl  15396  bpolydif  15399  fprodefsum  15438  dvdsmodexp  15605  dvdsaddre2b  15647  dvdsnprmd  16024  2mulprm  16027  prmndvdsfaclt  16057  ncoprmlnprm  16058  fermltl  16111  pceu  16173  setsstruct2  16511  setsstruct  16513  mreexexd  16909  isglbd  17717  pmtrfrn  18506  psgnunilem4  18545  ablsimpgprmd  19157  mulgass2  19271  islss4  19654  lspsneu  19815  lspfixed  19820  lspexch  19821  lsmcv  19833  lspsolvlem  19834  xrsdsreclblem  20510  isphld  20717  mdetralt  21136  mdetunilem9  21148  fiinopn  21428  neips  21640  tpnei  21648  neindisj2  21650  opnneiid  21653  hausnei2  21880  cmpsublem  21926  cmpsub  21927  cmpcld  21929  comppfsc  22059  filufint  22447  cfinufil  22455  rnelfm  22480  alexsubALTlem1  22574  alexsubALTlem4  22577  alexsubALT  22578  tsmsxp  22681  neibl  23029  tngngp3  23183  tgqioo  23326  ovolunlem2  24017  iunmbl2  24076  itg1le  24232  vieta1  24819  aannenlem2  24836  aalioulem3  24841  aalioulem4  24842  aaliou2  24847  wilthlem3  25564  bcmono  25770  gausslemma2dlem1a  25858  iscgrglt  26217  axcontlem7  26673  elntg2  26688  edglnl  26845  numedglnl  26846  ausgrumgri  26869  ausgrusgri  26870  usgrausgrb  26871  usgredg2vtxeuALT  26921  ushgredgedg  26928  ushgredgedgloop  26930  nbuhgr2vtx1edgb  27051  cusgrsize2inds  27152  upgrewlkle2  27305  wlkl1loop  27336  redwlk  27371  pthdivtx  27427  pthdadjvtx  27428  upgr2pthnlp  27430  upgrspthswlk  27436  clwlkl1loop  27481  wwlksnred  27587  wwlksnextbi  27589  elwwlks2ons3im  27650  umgrwwlks2on  27653  clwwlknwwlksn  27733  clwwlkinwwlk  27735  wwlksext2clwwlk  27753  1pthon2v  27849  uhgr3cyclex  27878  n4cyclfrgr  27987  frgrwopreg  28019  numclwwlk1lem2f1  28053  clwwlknonclwlknonf1o  28058  wlkl0  28063  frgrreggt1  28089  frgrreg  28090  frgrregord013  28091  chintcli  29025  spansnss  29265  elspansn4  29267  chscllem4  29334  hoadddir  29498  adjmul  29786  kbass6  29815  spansncv2  29987  sumdmdii  30109  nexple  31157  bnj1417  32200  lfuhgr2  32252  cusgredgex  32255  sat1el2xp  32513  fmlasuc  32520  satffunlem1lem1  32536  satffunlem2lem1  32538  mclsind  32704  iprodefisumlem  32859  poseq  32982  fpr3g  33009  frrlem10  33019  btwndiff  33375  elicc3  33552  finminlem  33553  sdclem2  34888  clmgmOLD  35000  grpomndo  35024  zerdivemp1x  35096  lsmsat  36014  lsmcv2  36035  lcvat  36036  lsatcveq0  36038  lcvexchlem4  36043  lcvexchlem5  36044  islshpcv  36059  l1cvpat  36060  lshpkrlem6  36121  omlfh3N  36265  cvlsupr4  36351  cvlsupr5  36352  cvlsupr6  36353  2llnneN  36415  hlrelat3  36418  cvrval3  36419  cvrval4N  36420  cvrexchlem  36425  2atlt  36445  cvrat4  36449  atbtwnexOLDN  36453  atbtwnex  36454  athgt  36462  3dim1  36473  3dim2  36474  3dim3  36475  1cvratex  36479  llnle  36524  atcvrlln2  36525  atcvrlln  36526  2llnmat  36530  lplnle  36546  lplnnle2at  36547  lplnnlelln  36549  llncvrlpln2  36563  2llnjN  36573  lvoli2  36587  lvolnlelln  36590  lvolnlelpln  36591  4atlem10  36612  4atlem11  36615  4atlem12  36618  lplncvrlvol2  36621  2lplnj  36626  lneq2at  36784  lnatexN  36785  lnjatN  36786  lncvrat  36788  2lnat  36790  cdlemb  36800  paddasslem14  36839  llnexchb2  36875  dalawlem10  36886  dalawlem13  36889  dalawlem14  36890  dalaw  36892  pclclN  36897  pclfinN  36906  osumcllem11N  36972  lhp2lt  37007  lhpexle3lem  37017  4atexlem7  37081  ldilcnv  37121  ldilco  37122  ltrncnv  37152  trlval2  37169  cdleme24  37358  cdleme26ee  37366  cdleme28  37379  cdleme32le  37453  cdleme50trn2  37557  cdleme50ltrn  37563  cdleme  37566  cdlemf1  37567  cdlemf  37569  cdlemg1cex  37594  cdlemg2ce  37598  cdlemg18b  37685  ltrnco  37725  tendocan  37830  cdlemk28-3  37914  cdlemk11t  37952  dia2dimlem6  38075  dia2dimlem12  38081  dihlsscpre  38240  dihord4  38264  dihord5b  38265  dihmeetlem3N  38311  dihmeetlem20N  38332  dvh4dimlem  38449  lclkrlem2y  38537  mapdpglem24  38710  mapdpglem32  38711  mapdpg  38712  baerlem3lem2  38716  baerlem5alem2  38717  baerlem5blem2  38718  mapdh9a  38795  mapdh9aOLDN  38796  hdmap14lem6  38879  hdmapglem7  38935  nnadddir  39031  nnmulcom  39033  nn0rppwr  39050  sn-addid2  39102  remulcand  39118  mzpexpmpt  39210  pellexlem5  39298  pellex  39300  pell14qrexpclnn0  39331  pellfundex  39351  monotuz  39406  monotoddzzfi  39407  rmxypos  39412  jm2.17a  39425  jm2.17b  39426  rmygeid  39429  jm2.19lem3  39456  jm2.15nn0  39468  jm2.16nn0  39469  aomclem2  39523  aomclem6  39527  dfac11  39530  hbtlem5  39596  cnsrexpcl  39633  relexpxpnnidm  39916  relexpiidm  39917  relexpss1d  39918  iunrelexpmin1  39921  relexpmulnn  39922  iunrelexpmin2  39925  relexp01min  39926  relexp0a  39929  relexpxpmin  39930  relexpaddss  39931  trclimalb2  39939  tfindsd  40432  3impexpbicomi  40682  ee333  40709  eel12131  40915  eel2122old  40920  e333  40935  ordelordALTVD  41069  refsumcn  41155  uzwo4  41183  ssinc  41221  ssdec  41222  iunincfi  41228  restuni3  41253  eliuniin2  41255  rabssd  41279  reximdd  41289  suprnmpt  41298  disjf1o  41320  fompt  41321  disjinfi  41322  ssnnf1octb  41324  choicefi  41331  mapssbi  41344  unirnmapsn  41345  ssmapsn  41347  iunmapsn  41348  funimassd  41365  rnmptlb  41382  rnmptbddlem  41383  infnsuprnmpt  41390  fperiodmullem  41438  upbdrech  41440  ssfiunibd  41444  supxrgere  41469  iuneqfzuzlem  41470  supxrgelem  41473  supxrge  41474  suplesup  41475  infrpge  41487  infleinf  41508  suplesup2  41512  supxrunb3  41540  infleinf2  41556  rexabslelem  41560  infrnmptle  41565  infxrunb3rnmpt  41570  iccshift  41662  iooshift  41666  fmul01  41729  fmuldfeq  41732  fmul01lt1  41735  mullimc  41765  islptre  41768  mullimcf  41772  limcperiod  41777  islpcn  41788  limsupre  41790  limcleqr  41793  neglimc  41796  addlimc  41797  0ellimcdiv  41798  limclner  41800  fnlimfvre  41823  limsuppnflem  41859  limsupmnfuzlem  41875  limsupre3lem  41881  limsupre3uzlem  41884  climuzlem  41892  limsupgtlem  41926  coskpi2  42015  cosknegpi  42018  cncfshift  42025  cncfperiod  42030  icccncfext  42038  dvnmptdivc  42091  dvnmptconst  42094  dvnmul  42096  dvmptfprodlem  42097  dvmptfprod  42098  dvnprodlem1  42099  dvnprodlem2  42100  iblspltprt  42126  itgspltprt  42132  itgperiod  42134  ismbl3  42140  stoweidlem3  42157  stoweidlem31  42185  stoweidlem59  42213  stirlinglem13  42240  fourierdlem41  42302  fourierdlem42  42303  fourierdlem48  42308  fourierdlem51  42311  fourierdlem53  42313  fourierdlem70  42330  fourierdlem71  42331  fourierdlem73  42333  fourierdlem80  42340  fourierdlem81  42341  fourierdlem89  42349  fourierdlem91  42351  fourierdlem93  42353  fourierdlem97  42357  elaa2  42388  qndenserrnopnlem  42451  salexct  42486  subsaliuncl  42510  subsalsal  42511  sge0tsms  42531  sge0f1o  42533  sge0fsum  42538  sge0supre  42540  sge0sup  42542  sge0rnbnd  42544  sge0gerp  42546  sge0pnffigt  42547  sge0lefi  42549  sge0ltfirp  42551  sge0resrn  42555  sge0resplit  42557  sge0split  42560  sge0iunmptlemfi  42564  sge0iunmptlemre  42566  sge0iunmpt  42569  sge0rpcpnf  42572  sge0isum  42578  sge0xp  42580  sge0xaddlem2  42585  sge0uzfsumgt  42595  sge0seq  42597  sge0reuz  42598  nnfoctbdjlem  42606  nnfoctbdj  42607  iundjiun  42611  meadjiunlem  42616  voliunsge0lem  42623  meaiuninclem  42631  meaiininc2  42639  carageniuncllem1  42672  carageniuncllem2  42673  caratheodorylem1  42677  caratheodorylem2  42678  isomenndlem  42681  ovnsupge0  42708  ovnlerp  42713  ovncvrrp  42715  ovnsubaddlem1  42721  hoidmvval0  42738  hoidmv1lelem3  42744  hoidmv1le  42745  hoidmvlelem1  42746  hoidmvlelem2  42747  hoidmvlelem3  42748  ovnhoilem2  42753  opnvonmbllem2  42784  ovolval5lem3  42805  ovnovollem3  42809  vonioo  42833  vonicc  42836  pimiooltgt  42858  sssmf  42884  smfaddlem1  42908  smflimlem6  42921  smfmullem4  42938  smfpimbor1lem1  42942  smfco  42946  smfpimcc  42951  smflimmpt  42953  smfinflem  42960  smflimsuplem7  42969  smflimsuplem8  42970  smflimsupmpt  42972  smfliminfmpt  42975  iccpartiltu  43417  sprsymrelfvlem  43487  reuopreuprim  43523  goldbachth  43544  fmtnofac1  43567  prmdvdsfmtnof1lem1  43581  lighneal  43611  isomgrsym  43836  isomgrtr  43839  uspgropssxp  43854  rngccatidALTV  44095  ringccatidALTV  44158  nzerooringczr  44178  lcosslsp  44328  fllog2  44463  dignn0flhalf  44513  itschlc0yqe  44582  itsclc0xyqsol  44590  iunord  44614  setrec2fun  44630
  Copyright terms: Public domain W3C validator