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 631 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  3expb  1114  3expiaOLD  1116  3expib  1117  3com12  1118  3com13  1119  syl3an2OLD  1169  syl3an3OLD  1171  ad4ant123OLD  1179  ad4ant124OLD  1181  ad4ant134OLD  1183  ad4ant234OLD  1185  pm3.2an3  1425  3expaOLD  1431  3com23OLD  1434  3imp3i2anOLD  1438  3an1rsOLD  1439  3exp1  1446  3expd  1447  exp5o  1449  ad5ant245OLD  1456  ad5ant234OLD  1458  ad5ant235OLD  1460  ad5ant123OLD  1462  ad5ant124OLD  1464  ad5ant125OLD  1466  ad5ant134OLD  1468  ad5ant135OLD  1470  ad5ant145OLD  1472  syl2an23anOLD  1535  3ecase  1586  rexlimdv3a  3171  rabssdv  3823  reupick2  4056  disjiund  4795  otiunsndisj  5130  wefrc  5260  predpo  5859  tz7.7  5910  unizlim  6005  fveqdmss  6517  f1oiso2  6765  ssorduni  7150  suceloni  7178  tfisi  7223  poxp  7457  smo11  7630  tfrlem5  7645  odi  7828  omass  7829  nndi  7872  nnmass  7873  undifixp  8110  findcard  8364  ac6sfi  8369  domunfican  8398  mapfien2  8479  fisup2g  8539  fiinf2g  8571  indcardi  9054  acndom  9064  ackbij1lem16  9249  infpssrlem4  9320  fin23lem11  9331  isfin2-2  9333  fin23lem34  9360  fin1a2lem10  9423  hsmexlem2  9441  axcc3  9452  domtriomlem  9456  axdc3lem2  9465  axdc3lem4  9467  axcclem  9471  ttukeyg  9531  axdclem2  9534  axacndlem4  9624  axacndlem5  9625  axacnd  9626  tskr1om2  9782  tskwe2  9787  tskord  9794  tskcard  9795  tskuni  9797  tskwun  9798  gruiin  9824  grudomon  9831  gruina  9832  mulcanpi  9914  adderpq  9970  mulerpq  9971  dedekindle  10393  divgt0  11083  divge0  11084  uzind  11661  uzind2  11662  iccsplit  12498  ssnn0fi  12978  sqlecan  13165  modexp  13193  facavg  13282  2cshwcshw  13771  relexpcnv  13974  relexpreld  13979  relexpaddnn  13990  relexpaddg  13992  prodfn0  14825  prodfrec  14826  ntrivcvgfvn0  14830  fprodabs  14903  fprodle  14926  bpolycl  14982  bpolydif  14985  fprodefsum  15024  dvdsmodexp  15190  dvdsaddre2b  15231  dvdsnprmd  15605  prmndvdsfaclt  15637  ncoprmlnprm  15638  fermltl  15691  pceu  15753  setsstruct2  16098  setsstruct  16100  mreexexd  16510  initoeu1  16862  termoeu1  16869  isglbd  17318  mulgaddcom  17765  pmtrfrn  18078  psgnunilem4  18117  mulgass2  18801  islss4  19164  lspsneu  19325  lspfixed  19330  lspexch  19331  lsmcv  19343  lspsolvlem  19344  xrsdsreclblem  19994  isphld  20201  mdetralt  20616  mdetunilem9  20628  fiinopn  20908  neips  21119  tpnei  21127  neindisj2  21129  opnneiid  21132  hausnei2  21359  cmpsublem  21404  cmpsub  21405  cmpcld  21407  comppfsc  21537  filufint  21925  cfinufil  21933  rnelfm  21958  alexsubALTlem1  22052  alexsubALTlem4  22055  alexsubALT  22056  tsmsxp  22159  neibl  22507  tngngp3  22661  tgqioo  22804  ovolunlem2  23466  iunmbl2  23525  itg1le  23679  vieta1  24266  aannenlem2  24283  aalioulem3  24288  aalioulem4  24289  aaliou2  24294  wilthlem3  24995  bcmono  25201  gausslemma2dlem1a  25289  axcontlem7  26049  edglnl  26237  numedglnl  26238  ausgrumgri  26261  ausgrusgri  26262  usgrausgrb  26263  usgredg2vtxeuALT  26313  ushgredgedg  26320  ushgredgedgloop  26322  nbuhgr2vtx1edgb  26447  cusgrsize2inds  26559  upgrewlkle2  26712  wlkl1loop  26744  redwlk  26779  pthdivtx  26835  pthdadjvtx  26836  upgr2pthnlp  26838  upgrspthswlk  26844  clwlkl1loop  26889  wwlksnred  27010  wwlksnextbi  27012  elwwlks2ons3im  27074  elwwlks2ons3OLD  27076  umgrwwlks2on  27078  clwwlknwwlksn  27166  clwwlknwwlksnOLD  27167  clwwlkinwwlk  27169  wwlksext2clwwlk  27187  clwlksfclwwlkOLD  27216  1pthon2v  27305  uhgr3cyclex  27334  n4cyclfrgr  27445  frgrwopreg  27477  numclwlk1lem2f1  27516  clwwlknonclwlknonf1o  27522  wlkl0  27528  frgrreggt1  27561  frgrreg  27562  frgrregord013  27563  chintcli  28499  spansnss  28739  elspansn4  28741  chscllem4  28808  hoadddir  28972  adjmul  29260  kbass6  29289  spansncv2  29461  sumdmdii  29583  nexple  30380  bnj1417  31416  mclsind  31774  iprodefisumlem  31933  poseq  32059  btwndiff  32440  elicc3  32617  finminlem  32618  sdclem2  33851  clmgmOLD  33963  grpomndo  33987  zerdivemp1x  34059  lsmsat  34798  lsmcv2  34819  lcvat  34820  lsatcveq0  34822  lcvexchlem4  34827  lcvexchlem5  34828  islshpcv  34843  l1cvpat  34844  lshpkrlem6  34905  omlfh3N  35049  cvlsupr4  35135  cvlsupr5  35136  cvlsupr6  35137  2llnneN  35198  hlrelat3  35201  cvrval3  35202  cvrval4N  35203  cvrexchlem  35208  2atlt  35228  cvrat4  35232  atbtwnexOLDN  35236  atbtwnex  35237  athgt  35245  3dim1  35256  3dim2  35257  3dim3  35258  1cvratex  35262  llnle  35307  atcvrlln2  35308  atcvrlln  35309  2llnmat  35313  lplnle  35329  lplnnle2at  35330  lplnnlelln  35332  llncvrlpln2  35346  2llnjN  35356  lvoli2  35370  lvolnlelln  35373  lvolnlelpln  35374  4atlem10  35395  4atlem11  35398  4atlem12  35401  lplncvrlvol2  35404  2lplnj  35409  lneq2at  35567  lnatexN  35568  lnjatN  35569  lncvrat  35571  2lnat  35573  cdlemb  35583  paddasslem14  35622  llnexchb2  35658  dalawlem10  35669  dalawlem13  35672  dalawlem14  35673  dalaw  35675  pclclN  35680  pclfinN  35689  osumcllem11N  35755  lhp2lt  35790  lhpexle3lem  35800  4atexlem7  35864  ldilcnv  35904  ldilco  35905  ltrncnv  35935  trlval2  35953  cdleme24  36142  cdleme26ee  36150  cdleme28  36163  cdleme32le  36237  cdleme50trn2  36341  cdleme50ltrn  36347  cdleme  36350  cdlemf1  36351  cdlemf  36353  cdlemg1cex  36378  cdlemg2ce  36382  cdlemg18b  36469  ltrnco  36509  tendocan  36614  cdlemk28-3  36698  cdlemk11t  36736  dia2dimlem6  36860  dia2dimlem12  36866  dihlsscpre  37025  dihord4  37049  dihord5b  37050  dihmeetlem3N  37096  dihmeetlem20N  37117  dvh4dimlem  37234  lclkrlem2y  37322  mapdpglem24  37495  mapdpglem32  37496  mapdpg  37497  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  mapdh9a  37581  mapdh9aOLDN  37582  hdmap14lem6  37667  hdmapglem7  37723  mzpexpmpt  37810  pellexlem5  37899  pellex  37901  pell14qrexpclnn0  37932  pellfundex  37952  monotuz  38008  monotoddzzfi  38009  expmordi  38014  rmxypos  38016  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  jm2.19lem3  38060  jm2.15nn0  38072  jm2.16nn0  38073  aomclem2  38127  aomclem6  38131  dfac11  38134  hbtlem5  38200  cnsrexpcl  38237  relexpxpnnidm  38497  relexpiidm  38498  relexpss1d  38499  iunrelexpmin1  38502  relexpmulnn  38503  iunrelexpmin2  38506  relexp01min  38507  relexp0a  38510  relexpxpmin  38511  relexpaddss  38512  trclimalb2  38520  3impexpbicomi  39188  ee333  39215  eel12131  39440  eel2122old  39445  e333  39462  ordelordALTVD  39602  refsumcn  39688  uzwo4  39720  ssinc  39763  ssdec  39764  iunincfi  39771  restuni3  39800  eliuniin2  39802  rabssd  39831  reximdd  39843  suprnmpt  39854  wessf1ornlem  39870  disjf1o  39877  fompt  39878  disjinfi  39879  ssnnf1octb  39881  mapsnd  39887  choicefi  39891  mapssbi  39904  unirnmapsn  39905  ssmapsn  39907  iunmapsn  39908  funimassd  39930  rnmptlb  39952  rnmptbddlem  39954  fvelimad  39957  infnsuprnmpt  39964  fperiodmullem  40016  upbdrech  40018  ssfiunibd  40022  supxrgere  40047  iuneqfzuzlem  40048  supxrgelem  40051  supxrge  40052  suplesup  40053  infrpge  40065  infleinf  40086  suplesup2  40090  supxrunb3  40121  infleinf2  40139  rexabslelem  40143  infrnmptle  40148  infxrunb3rnmpt  40153  iccshift  40247  iooshift  40251  fmul01  40315  fmuldfeq  40318  fmul01lt1  40321  mullimc  40351  islptre  40354  mullimcf  40358  limcperiod  40363  islpcn  40374  limsupre  40376  limcleqr  40379  neglimc  40382  addlimc  40383  0ellimcdiv  40384  limclner  40386  fnlimfvre  40409  limsuppnflem  40445  limsupmnfuzlem  40461  limsupre3lem  40467  limsupre3uzlem  40470  climuzlem  40478  limsupgtlem  40512  coskpi2  40580  cosknegpi  40583  cncfshift  40590  cncfperiod  40595  icccncfext  40603  dvnmptdivc  40656  dvnmptconst  40659  dvnmul  40661  dvmptfprodlem  40662  dvmptfprod  40663  dvnprodlem1  40664  dvnprodlem2  40665  iblspltprt  40692  itgspltprt  40698  itgperiod  40700  ismbl3  40706  stoweidlem3  40723  stoweidlem31  40751  stoweidlem59  40779  stirlinglem13  40806  fourierdlem41  40868  fourierdlem42  40869  fourierdlem48  40874  fourierdlem51  40877  fourierdlem53  40879  fourierdlem70  40896  fourierdlem71  40897  fourierdlem73  40899  fourierdlem80  40906  fourierdlem81  40907  fourierdlem89  40915  fourierdlem91  40917  fourierdlem93  40919  fourierdlem97  40923  elaa2  40954  qndenserrnopnlem  41020  salexct  41055  subsaliuncl  41079  subsalsal  41080  sge0tsms  41100  sge0f1o  41102  sge0fsum  41107  sge0supre  41109  sge0sup  41111  sge0rnbnd  41113  sge0gerp  41115  sge0pnffigt  41116  sge0lefi  41118  sge0ltfirp  41120  sge0resrn  41124  sge0resplit  41126  sge0split  41129  sge0iunmptlemfi  41133  sge0iunmptlemre  41135  sge0iunmpt  41138  sge0rpcpnf  41141  sge0isum  41147  sge0xp  41149  sge0xaddlem2  41154  sge0uzfsumgt  41164  sge0seq  41166  sge0reuz  41167  nnfoctbdjlem  41175  nnfoctbdj  41176  iundjiun  41180  meadjiunlem  41185  voliunsge0lem  41192  meaiuninclem  41200  meaiininc2  41208  carageniuncllem1  41241  carageniuncllem2  41242  caratheodorylem1  41246  caratheodorylem2  41247  isomenndlem  41250  ovnsupge0  41277  ovnlerp  41282  ovncvrrp  41284  ovnsubaddlem1  41290  hoidmvval0  41307  hoidmv1lelem3  41313  hoidmv1le  41314  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  ovnhoilem2  41322  opnvonmbllem2  41353  ovolval5lem3  41374  ovnovollem3  41378  vonioo  41402  vonicc  41405  pimiooltgt  41427  sssmf  41453  smfaddlem1  41477  smflimlem6  41490  smfmullem4  41507  smfpimbor1lem1  41511  smfco  41515  smfpimcc  41520  smflimmpt  41522  smfinflem  41529  smflimsuplem7  41538  smflimsuplem8  41539  smflimsupmpt  41541  smfliminfmpt  41544  iccpartiltu  41868  goldbachth  41969  fmtnofac1  41992  prmdvdsfmtnof1lem1  42006  pwdif  42011  lighneal  42038  sprsymrelfvlem  42250  uspgropssxp  42262  rngccatidALTV  42499  ringccatidALTV  42562  nzerooringczr  42582  lcosslsp  42737  fllog2  42872  dignn0flhalf  42922  iunord  42932  setrec2fun  42949
  Copyright terms: Public domain W3C validator