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

Theorem exp31 422
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 415 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 415 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  exp41  437  exp42  438  imp5a  443  expl  460  anasss  469  an31s  652  exbiri  809  3exp  1113  exp516  1350  rexlimdva2  3285  r19.29af2  3328  reusv2lem2  5290  pwssun  5448  onmindif  6273  mpteqb  6780  fliftfun  7057  elovmpt3rab1  7397  ordsucss  7525  tfindsg  7567  imacosuppOLD  7867  tfrlem1  8004  tfrlem9  8013  oaordi  8164  oaordex  8176  oaass  8179  oarec  8180  omass  8198  oen0  8204  oeordsuc  8212  nnaordi  8236  omsmolem  8272  infensuc  8687  php3  8695  suppeqfsuppbi  8839  marypha1lem  8889  hartogs  9000  card2on  9010  tz9.12lem3  9210  infxpenlem  9431  cfcoflem  9686  isf32lem12  9778  zorn2lem6  9915  ondomon  9977  axrepnd  10008  fpwwe2lem12  10055  genpcd  10420  ltexprlem6  10455  axpre-sup  10583  negf1o  11062  recex  11264  fiminreOLD  11582  uzaddcl  12296  nn01to3  12333  rpnnen1lem5  12372  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  supxrunb2  12705  fz0fzelfz0  13005  fz0fzdiffz0  13008  elfzmlbp  13010  difelfzle  13012  fzo1fzo0n0  13080  elincfzoext  13087  ssfzo12bi  13124  elfznelfzo  13134  modaddmodup  13294  modfzo0difsn  13303  fsuppmapnn0fiubex  13352  seqf1o  13403  expcllem  13432  expeq0  13451  mulexp  13460  hashgt12el2  13776  hashimarni  13794  hash2prd  13825  fi1uzind  13847  swrdnd  14008  swrdswrdlem  14058  swrdswrd  14059  pfxccat3  14088  reuccatpfxs1  14101  repswswrd  14138  repswccat  14140  cshwidxmod  14157  2cshwcshw  14179  s4f1o  14272  wwlktovfo  14314  resqrex  14602  summo  15066  fsum2d  15118  modfsummods  15140  binom  15177  clim2prod  15236  fprod2d  15327  binomfallfac  15387  efexp  15446  demoivreALT  15546  divconjdvds  15657  addmodlteqALT  15667  dfgcd2  15886  lcmfunsnlem2lem1  15974  lcmfdvdsb  15979  lcmfun  15981  coprmprod  15997  coprmproddvdslem  15998  oddprmdvds  16231  ramcl  16357  prmgaplem6  16384  cshwsidrepswmod0  16420  cshwshashlem1  16421  cshwshashlem2  16422  ressress  16554  initoeu2lem1  17266  symggen  18590  pmtr3ncom  18595  srgmulgass  19273  srgbinom  19287  ringinvnzdiv  19335  lmodvsmmulgdi  19661  assamulgscmlem2  20121  mptcoe1fsupp  20375  coe1fzgsumdlem  20461  evl1gsumdlem  20511  psgndiflemB  20736  scmatmulcl  21119  mdetdiagid  21201  pm2mpf1  21399  mptcoe1matfsupp  21402  mp2pm2mplem4  21409  chpdmat  21441  chfacfisf  21454  chfacfisfcpmat  21455  chcoeffeq  21486  topbas  21572  elcls  21673  elcls3  21683  2ndcdisj  22056  filufint  22520  ovoliunlem3  24097  dvge0  24595  ulmcn  24979  gausslemma2dlem3  25936  sizusglecusg  27237  upgriswlk  27414  2pthnloop  27504  crctcshwlkn0  27591  wlknwwlksnbij  27658  wwlksnred  27662  wwlksnext  27663  wwlksnextinj  27669  wwlksnextproplem2  27681  wwlksnextproplem3  27682  usgr2wspthons3  27735  clwwlkccatlem  27759  clwlkclwwlklem2a4  27767  clwlkclwwlklem2a  27768  clwlkclwwlklem2  27770  erclwwlktr  27792  clwwlkinwwlk  27810  clwwlkf  27818  clwwlkf1  27820  wwlksext2clwwlk  27828  clwwlknscsh  27833  umgr2cwwk2dif  27835  erclwwlkntr  27842  clwwlknonex2  27880  uhgr3cyclex  27953  upgr4cycl4dv4e  27956  eucrctshift  28014  3cyclfrgrrn1  28056  frgrwopreglem2  28084  frgrwopreglem5  28092  frgrwopreglem5ALT  28093  numclwwlk1lem2fo  28129  numclwlk2lem2f  28148  numclwlk2lem2f1o  28150  frgrreg  28165  friendshipgt3  28169  friendship  28170  ipasslem1  28600  shmodsi  29158  elspansn5  29343  h1datomi  29350  nmopsetretALT  29632  pjss2coi  29933  pj3cor1i  29978  mdexchi  30104  atcvat4i  30166  mdsymlem3  30174  mdsymlem4  30175  sumdmdii  30184  cdj3lem2b  30206  elabreximd  30262  iuninc  30304  iundisjf  30331  xrsmulgzz  30658  gsumle  30718  gsumvsca1  30847  gsumvsca2  30848  ofldchr  30880  locfinreflem  31097  xrge0iifiso  31171  lmxrge0  31188  esumfzf  31321  sigaclfu2  31373  signstfvneq0  31835  satfrel  32607  satfrnmapom  32610  fmlafvel  32625  fmlasuc  32626  bccolsum  32964  faclimlem1  32968  dftrpred3g  33065  nosupbnd1  33207  nosupbnd2  33209  segletr  33568  segleantisym  33569  outsideoftr  33583  exp5d  33643  elicc3  33658  finxpreclem2  34663  wl-sbcom2d  34789  poimirlem26  34910  mblfinlem3  34923  itg2addnc  34938  indexa  35000  ax12indalem  36073  ax12inda2ALT  36074  cvrat4  36571  elpaddn0  36928  paddasslem5  36952  paddasslem14  36961  eldioph2  39349  pell1234qrdich  39448  gneispb  40471  rexlimd3  41402  rexabslelem  41681  climsuselem1  41877  stoweidlem19  42294  stoweidlem20  42295  stoweidlem34  42309  wallispilem3  42342  sge0iunmpt  42690  meaiuninc3v  42756  smflimmpt  43074  or2expropbilem1  43257  2reu8i  43302  2elfz2melfz  43508  subsubelfzo0  43516  iccpartigtl  43573  iccpartgt  43577  icceuelpartlem  43585  fargshiftf1  43591  ich2exprop  43623  ichreuopeq  43625  lighneallem3  43762  gbowgt5  43917  bgoldbtbndlem3  43962  bgoldbtbndlem4  43963  bgoldbtbnd  43964  tgblthelfgott  43970  isomuspgrlem2b  43984  upgrwlkupwlk  44005  2zrngagrp  44204  rhmsubcrngclem2  44289  nzerooringczr  44333  lmodvsmdi  44420  ply1mulgsumlem1  44430  elfzolborelfzop1  44564  nnolog2flm1  44640  nn0sumshdiglemA  44669  eenglngeehlnmlem2  44715
  Copyright terms: Public domain W3C validator