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

Theorem exp31 630
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 450 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 450 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  exp41  638  exp42  639  expl  648  exbiri  652  anasss  679  an31s  848  pm3.2an3  1239  3impa  1258  exp516  1286  r19.29af2  3073  reusv2lem2  4867  pwssun  5018  onmindif  5813  mpteqb  6297  dffo3  6372  fliftfun  6559  elovmpt3rab1  6890  ordsucss  7015  tfindsg  7057  imacosupp  7332  tfrlem1  7469  tfrlem9  7478  oaordi  7623  oaordex  7635  oaass  7638  oarec  7639  omlimcl  7655  omass  7657  oen0  7663  oeordsuc  7671  nnaordi  7695  omsmolem  7730  infensuc  8135  php3  8143  suppeqfsuppbi  8286  marypha1lem  8336  hartogs  8446  card2on  8456  tz9.12lem3  8649  infxpenlem  8833  cfflb  9078  cfcoflem  9091  cfcof  9093  isf32lem12  9183  zorn2lem6  9320  ondomon  9382  alephval2  9391  pwcfsdom  9402  axrepnd  9413  fpwwe2lem12  9460  genpcd  9825  ltexprlem6  9860  recexsr  9925  axpre-sup  9987  negf1o  10457  recex  10656  zdiv  11444  uzaddcl  11741  nn01to3  11778  rpnnen1lem5  11815  rpnnen1lem5OLD  11821  xrsupsslem  12134  xrinfmsslem  12135  supxrunb1  12146  supxrunb2  12147  fz0fzelfz0  12441  fz0fzdiffz0  12444  elfzmlbp  12446  difelfzle  12448  fzo1fzo0n0  12514  elincfzoext  12521  ssfzo12bi  12559  elfznelfzo  12569  modaddmodup  12728  modfzo0difsn  12737  fsuppmapnn0fiubex  12787  seqf1o  12837  expcllem  12866  expeq0  12885  mulexp  12894  hashgt12el2  13206  hashimarni  13223  hash2prd  13252  fi1uzind  13274  fi1uzindOLD  13280  swrdnd  13426  swrdswrdlem  13453  swrdswrd  13454  reuccats1  13474  swrdccat3  13486  swrdccatid  13491  repswswrd  13525  repswccat  13526  cshwidxmod  13543  2cshwcshw  13565  s4f1o  13657  wwlktovfo  13695  cjexp  13884  resqrex  13985  absexp  14038  summo  14442  fsum2d  14496  modfsummods  14519  binom  14556  clim2prod  14614  fprod2d  14705  binomfallfac  14766  efexp  14825  demoivreALT  14925  divconjdvds  15031  addmodlteqALT  15041  dfgcd2  15257  lcmfunsnlem2lem1  15345  lcmfdvdsb  15350  lcmfun  15352  coprmprod  15369  coprmproddvdslem  15370  oddprmdvds  15601  ramcl  15727  cshwsidrepswmod0  15795  cshwshashlem1  15796  ressress  15932  initoeu2lem1  16658  symggen  17884  pmtr3ncom  17889  srgmulgass  18525  srgbinom  18539  ringinvnzdiv  18587  lmodvsmmulgdi  18892  assamulgscmlem2  19343  mptcoe1fsupp  19579  coe1fzgsumdlem  19665  evl1gsumdlem  19714  psgndiflemB  19940  scmatmulcl  20318  mdetdiagid  20400  pm2mpf1  20598  mptcoe1matfsupp  20601  mp2pm2mplem4  20608  chpdmat  20640  chfacfisf  20653  chfacfisfcpmat  20654  chcoeffeq  20685  topbas  20770  fctop  20802  cctop  20804  elcls  20871  elcls3  20881  2ndcdisj  21253  filufint  21718  ovoliunlem3  23266  dvge0  23763  ulmcn  24147  gausslemma2dlem3  25087  sizusglecusg  26353  upgriswlk  26531  2pthnloop  26621  crctcshwlkn0  26707  wwlksnred  26781  wwlksnextinj  26788  wwlksnextproplem2  26799  wwlksnextproplem3  26800  wwlks2onv  26841  usgr2wspthons3  26851  clwlkclwwlklem2a4  26892  clwlkclwwlklem2a  26893  clwlkclwwlklem2  26895  clwwlksf  26908  clwwlksf1  26910  wwlksext2clwwlk  26917  erclwwlkstr  26929  clwwlksnscsh  26933  umgr2cwwk2dif  26934  erclwwlksntr  26941  clwlksfclwwlk  26955  clwlksf1clwwlklem  26961  uhgr3cyclex  27035  upgr4cycl4dv4e  27038  eucrctshift  27096  3cyclfrgrrn1  27142  frgrwopreglem2  27168  frgrwopreglem5  27171  extwwlkfablem2  27197  numclwwlkovf2ex  27204  numclwlk1lem2foa  27208  numclwlk1lem2fo  27212  numclwlk2lem2f  27220  numclwlk2lem2f1o  27222  frgrreg  27236  friendshipgt3  27240  friendship  27241  grpoinvf  27370  nmosetre  27603  ipasslem1  27670  shmodsi  28232  elspansn5  28417  normcan  28419  h1datomi  28424  nmopsetretALT  28706  nmfnsetre  28720  pjss2coi  29007  pj3cor1i  29052  mdexchi  29178  superpos  29197  atcvat4i  29240  mdsymlem3  29248  mdsymlem4  29249  sumdmdii  29258  cdj3lem2b  29280  elabreximd  29332  iuninc  29363  iundisjf  29386  xrsmulgzz  29663  gsumle  29764  gsumvsca1  29767  gsumvsca2  29768  ofldchr  29799  locfinreflem  29892  xrge0iifiso  29966  lmxrge0  29983  esumfzf  30116  sigaclfu2  30169  eulerpartlemgh  30425  signstfvneq0  30634  signstfvc  30636  bccolsum  31611  faclimlem1  31615  dftrpred3g  31717  nosupbnd1  31844  nosupbnd2  31846  segletr  32205  segleantisym  32206  outsideoftr  32220  exp5d  32280  elicc3  32295  finxpreclem2  33207  wl-sbcom2d  33324  poimirlem26  33415  mblfinlem3  33428  itg2addnc  33444  indexa  33508  ax12indalem  34056  ax12inda2ALT  34057  cvrat4  34555  elpaddn0  34912  paddasslem5  34936  paddasslem14  34945  eldioph2  37151  pell1234qrdich  37251  gneispb  38255  rexlimd3  39161  rexlimdva2  39165  dffo3f  39186  rnmptlb  39275  rexabslelem  39464  climsuselem1  39645  limsupubuz  39751  stoweidlem19  40005  stoweidlem20  40006  stoweidlem34  40020  wallispilem3  40053  sge0iunmpt  40404  smflimlem4  40751  smflimmpt  40785  2elfz2melfz  41097  subsubelfzo0  41105  iccpartigtl  41129  iccpartgt  41133  icceuelpartlem  41141  fargshiftf1  41147  pfxccat3  41197  lighneallem3  41295  gbowgt5  41421  mogoldbb  41444  bgoldbtbndlem3  41466  bgoldbtbndlem4  41467  bgoldbtbnd  41468  tgblthelfgott  41474  tgblthelfgottOLD  41480  upgrwlkupwlk  41492  2zrngagrp  41714  rhmsubcrngclem2  41799  nzerooringczr  41843  lmodvsmdi  41934  ply1mulgsumlem1  41945  islindeps2  42043  elfzolborelfzop1  42080  nnolog2flm1  42155  nn0sumshdiglemA  42184
  Copyright terms: Public domain W3C validator