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

Theorem exp31 420
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 413 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 413 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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
This theorem is referenced by:  exp41  435  exp42  436  imp5a  441  expl  458  anasss  467  an31s  650  exbiri  807  3exp  1111  exp516  1348  rexlimdva2  3287  r19.29af2  3330  reusv2lem2  5291  pwssun  5449  onmindif  6274  mpteqb  6780  fliftfun  7054  elovmpt3rab1  7394  ordsucss  7521  tfindsg  7563  imacosuppOLD  7866  tfrlem1  8003  tfrlem9  8012  oaordi  8162  oaordex  8174  oaass  8177  oarec  8178  omass  8196  oen0  8202  oeordsuc  8210  nnaordi  8234  omsmolem  8270  infensuc  8684  php3  8692  suppeqfsuppbi  8836  marypha1lem  8886  hartogs  8997  card2on  9007  tz9.12lem3  9207  infxpenlem  9428  cfcoflem  9683  isf32lem12  9775  zorn2lem6  9912  ondomon  9974  axrepnd  10005  fpwwe2lem12  10052  genpcd  10417  ltexprlem6  10452  axpre-sup  10580  negf1o  11059  recex  11261  fiminreOLD  11579  uzaddcl  12293  nn01to3  12330  rpnnen1lem5  12370  xrsupsslem  12690  xrinfmsslem  12691  supxrunb1  12702  supxrunb2  12703  fz0fzelfz0  13003  fz0fzdiffz0  13006  elfzmlbp  13008  difelfzle  13010  fzo1fzo0n0  13078  elincfzoext  13085  ssfzo12bi  13122  elfznelfzo  13132  modaddmodup  13292  modfzo0difsn  13301  fsuppmapnn0fiubex  13350  seqf1o  13401  expcllem  13430  expeq0  13449  mulexp  13458  hashgt12el2  13774  hashimarni  13792  hash2prd  13823  fi1uzind  13845  swrdnd  14006  swrdswrdlem  14056  swrdswrd  14057  pfxccat3  14086  reuccatpfxs1  14099  repswswrd  14136  repswccat  14138  cshwidxmod  14155  2cshwcshw  14177  s4f1o  14270  wwlktovfo  14312  resqrex  14600  summo  15064  fsum2d  15116  modfsummods  15138  binom  15175  clim2prod  15234  fprod2d  15325  binomfallfac  15385  efexp  15444  demoivreALT  15544  divconjdvds  15655  addmodlteqALT  15665  dfgcd2  15884  lcmfunsnlem2lem1  15972  lcmfdvdsb  15977  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  oddprmdvds  16229  ramcl  16355  prmgaplem6  16382  cshwsidrepswmod0  16418  cshwshashlem1  16419  cshwshashlem2  16420  ressress  16552  initoeu2lem1  17264  symggen  18529  pmtr3ncom  18534  srgmulgass  19212  srgbinom  19226  ringinvnzdiv  19274  lmodvsmmulgdi  19600  assamulgscmlem2  20059  mptcoe1fsupp  20313  coe1fzgsumdlem  20399  evl1gsumdlem  20449  psgndiflemB  20674  scmatmulcl  21057  mdetdiagid  21139  pm2mpf1  21337  mptcoe1matfsupp  21340  mp2pm2mplem4  21347  chpdmat  21379  chfacfisf  21392  chfacfisfcpmat  21393  chcoeffeq  21424  topbas  21510  elcls  21611  elcls3  21621  2ndcdisj  21994  filufint  22458  ovoliunlem3  24034  dvge0  24532  ulmcn  24916  gausslemma2dlem3  25872  sizusglecusg  27173  upgriswlk  27350  2pthnloop  27440  crctcshwlkn0  27527  wlknwwlksnbij  27594  wwlksnred  27598  wwlksnext  27599  wwlksnextinj  27605  wwlksnextproplem2  27617  wwlksnextproplem3  27618  usgr2wspthons3  27671  clwwlkccatlem  27695  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  erclwwlktr  27728  clwwlkinwwlk  27746  clwwlkf  27754  clwwlkf1  27756  wwlksext2clwwlk  27764  clwwlknscsh  27769  umgr2cwwk2dif  27771  erclwwlkntr  27778  clwwlknonex2  27816  uhgr3cyclex  27889  upgr4cycl4dv4e  27892  eucrctshift  27950  3cyclfrgrrn1  27992  frgrwopreglem2  28020  frgrwopreglem5  28028  frgrwopreglem5ALT  28029  numclwwlk1lem2fo  28065  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  frgrreg  28101  friendshipgt3  28105  friendship  28106  ipasslem1  28536  shmodsi  29094  elspansn5  29279  h1datomi  29286  nmopsetretALT  29568  pjss2coi  29869  pj3cor1i  29914  mdexchi  30040  atcvat4i  30102  mdsymlem3  30110  mdsymlem4  30111  sumdmdii  30120  cdj3lem2b  30142  elabreximd  30198  iuninc  30241  iundisjf  30268  xrsmulgzz  30593  gsumle  30653  gsumvsca1  30782  gsumvsca2  30783  ofldchr  30815  locfinreflem  31004  xrge0iifiso  31078  lmxrge0  31095  esumfzf  31228  sigaclfu2  31280  signstfvneq0  31742  satfrel  32512  satfrnmapom  32515  fmlafvel  32530  fmlasuc  32531  bccolsum  32869  faclimlem1  32873  dftrpred3g  32970  nosupbnd1  33112  nosupbnd2  33114  segletr  33473  segleantisym  33474  outsideoftr  33488  exp5d  33548  elicc3  33563  finxpreclem2  34554  wl-sbcom2d  34679  poimirlem26  34800  mblfinlem3  34813  itg2addnc  34828  indexa  34891  ax12indalem  35963  ax12inda2ALT  35964  cvrat4  36461  elpaddn0  36818  paddasslem5  36842  paddasslem14  36851  eldioph2  39239  pell1234qrdich  39338  gneispb  40361  rexlimd3  41293  rexabslelem  41572  climsuselem1  41768  stoweidlem19  42185  stoweidlem20  42186  stoweidlem34  42200  wallispilem3  42233  sge0iunmpt  42581  meaiuninc3v  42647  smflimmpt  42965  or2expropbilem1  43148  2reu8i  43193  2elfz2melfz  43399  subsubelfzo0  43407  iccpartigtl  43430  iccpartgt  43434  icceuelpartlem  43442  fargshiftf1  43448  ich2exprop  43480  ichreuopeq  43482  lighneallem3  43619  gbowgt5  43774  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgblthelfgott  43827  isomuspgrlem2b  43841  upgrwlkupwlk  43862  2zrngagrp  44112  rhmsubcrngclem2  44197  nzerooringczr  44241  lmodvsmdi  44328  ply1mulgsumlem1  44338  elfzolborelfzop1  44472  nnolog2flm1  44548  nn0sumshdiglemA  44577  eenglngeehlnmlem2  44623
  Copyright terms: Public domain W3C validator