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

Theorem exp31 629
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp31.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
exp31 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21ex 449 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 449 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  exp41  637  exp42  638  expl  647  exbiri  651  anasss  680  an31s  865  pm3.2an3  1260  3impa  1278  exp516  1309  r19.29af2  3104  reusv2lem2  4899  pwssun  5049  onmindif  5853  mpteqb  6338  dffo3  6414  fliftfun  6602  elovmpt3rab1  6935  ordsucss  7060  tfindsg  7102  imacosupp  7380  tfrlem1  7517  tfrlem9  7526  oaordi  7671  oaordex  7683  oaass  7686  oarec  7687  omlimcl  7703  omass  7705  oen0  7711  oeordsuc  7719  nnaordi  7743  omsmolem  7778  infensuc  8179  php3  8187  suppeqfsuppbi  8330  marypha1lem  8380  hartogs  8490  card2on  8500  tz9.12lem3  8690  infxpenlem  8874  cfflb  9119  cfcoflem  9132  cfcof  9134  isf32lem12  9224  zorn2lem6  9361  ondomon  9423  alephval2  9432  pwcfsdom  9443  axrepnd  9454  fpwwe2lem12  9501  genpcd  9866  ltexprlem6  9901  recexsr  9966  axpre-sup  10028  negf1o  10498  recex  10697  zdiv  11485  uzaddcl  11782  nn01to3  11819  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  fz0fzelfz0  12484  fz0fzdiffz0  12487  elfzmlbp  12489  difelfzle  12491  fzo1fzo0n0  12558  elincfzoext  12565  ssfzo12bi  12603  elfznelfzo  12613  modaddmodup  12773  modfzo0difsn  12782  fsuppmapnn0fiubex  12832  seqf1o  12882  expcllem  12911  expeq0  12930  mulexp  12939  hashgt12el2  13249  hashimarni  13266  hash2prd  13295  fi1uzind  13317  swrdnd  13478  swrdswrdlem  13505  swrdswrd  13506  reuccats1  13526  swrdccat3  13538  swrdccatid  13543  repswswrd  13577  repswccat  13578  cshwidxmod  13595  2cshwcshw  13617  s4f1o  13709  wwlktovfo  13747  cjexp  13934  resqrex  14035  absexp  14088  summo  14492  fsum2d  14546  modfsummods  14569  binom  14606  clim2prod  14664  fprod2d  14755  binomfallfac  14816  efexp  14875  demoivreALT  14975  divconjdvds  15084  addmodlteqALT  15094  dfgcd2  15310  lcmfunsnlem2lem1  15398  lcmfdvdsb  15403  lcmfun  15405  coprmprod  15422  coprmproddvdslem  15423  oddprmdvds  15654  ramcl  15780  cshwsidrepswmod0  15848  cshwshashlem1  15849  ressress  15985  initoeu2lem1  16711  symggen  17936  pmtr3ncom  17941  srgmulgass  18577  srgbinom  18591  ringinvnzdiv  18639  lmodvsmmulgdi  18946  assamulgscmlem2  19397  mptcoe1fsupp  19633  coe1fzgsumdlem  19719  evl1gsumdlem  19768  psgndiflemB  19994  scmatmulcl  20372  mdetdiagid  20454  pm2mpf1  20652  mptcoe1matfsupp  20655  mp2pm2mplem4  20662  chpdmat  20694  chfacfisf  20707  chfacfisfcpmat  20708  chcoeffeq  20739  topbas  20824  fctop  20856  cctop  20858  elcls  20925  elcls3  20935  2ndcdisj  21307  filufint  21771  ovoliunlem3  23318  dvge0  23814  ulmcn  24198  gausslemma2dlem3  25138  sizusglecusg  26415  upgriswlk  26593  2pthnloop  26683  crctcshwlkn0  26769  wwlksnred  26855  wwlksnextinj  26862  wwlksnextproplem2  26873  wwlksnextproplem3  26874  usgr2wspthons3  26931  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  erclwwlktr  26979  clwwlkinwwlk  27003  clwwlkf  27010  clwwlkf1  27012  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwwlknscsh  27027  umgr2cwwk2dif  27028  erclwwlkntr  27035  clwlksfclwwlk  27049  clwlksf1clwwlklem  27055  clwwlknonex2  27084  uhgr3cyclex  27160  upgr4cycl4dv4e  27163  eucrctshift  27221  3cyclfrgrrn1  27265  frgrwopreglem2  27293  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  clwwlkccatlem  27331  numclwlk1lem2fo  27348  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  frgrreg  27381  friendshipgt3  27385  friendship  27386  grpoinvf  27514  nmosetre  27747  ipasslem1  27814  shmodsi  28376  elspansn5  28561  normcan  28563  h1datomi  28568  nmopsetretALT  28850  nmfnsetre  28864  pjss2coi  29151  pj3cor1i  29196  mdexchi  29322  superpos  29341  atcvat4i  29384  mdsymlem3  29392  mdsymlem4  29393  sumdmdii  29402  cdj3lem2b  29424  elabreximd  29474  iuninc  29505  iundisjf  29528  xrsmulgzz  29806  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  ofldchr  29942  locfinreflem  30035  xrge0iifiso  30109  lmxrge0  30126  esumfzf  30259  sigaclfu2  30312  eulerpartlemgh  30568  signstfvneq0  30777  signstfvc  30779  bccolsum  31751  faclimlem1  31755  dftrpred3g  31857  nosupbnd1  31985  nosupbnd2  31987  segletr  32346  segleantisym  32347  outsideoftr  32361  exp5d  32421  elicc3  32436  finxpreclem2  33357  wl-sbcom2d  33474  poimirlem26  33565  mblfinlem3  33578  itg2addnc  33594  indexa  33658  ax12indalem  34549  ax12inda2ALT  34550  cvrat4  35047  elpaddn0  35404  paddasslem5  35428  paddasslem14  35437  eldioph2  37642  pell1234qrdich  37742  gneispb  38746  rexlimd3  39649  rexlimdva2  39653  dffo3f  39678  rnmptlb  39767  rexabslelem  39958  climsuselem1  40157  limsupubuz  40263  stoweidlem19  40554  stoweidlem20  40555  stoweidlem34  40569  wallispilem3  40602  sge0iunmpt  40953  meaiuninc3v  41019  smflimlem4  41303  smflimmpt  41337  2elfz2melfz  41653  subsubelfzo0  41661  iccpartigtl  41684  iccpartgt  41688  icceuelpartlem  41696  fargshiftf1  41702  pfxccat3  41751  lighneallem3  41849  gbowgt5  41975  mogoldbb  41998  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  tgblthelfgott  42028  tgblthelfgottOLD  42034  upgrwlkupwlk  42046  2zrngagrp  42268  rhmsubcrngclem2  42353  nzerooringczr  42397  lmodvsmdi  42488  ply1mulgsumlem1  42499  islindeps2  42597  elfzolborelfzop1  42634  nnolog2flm1  42709  nn0sumshdiglemA  42738
  Copyright terms: Public domain W3C validator