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

Theorem exp31 406
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 397 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 397 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  exp41  421  exp42  422  imp5a  427  expl  445  anasss  457  an31s  625  exbiri  808  3impaOLD  1105  3exp  1111  pm3.2an3OLD  1424  exp516  1448  r19.29af2  3222  reusv2lem2  4997  pwssun  5153  onmindif  5958  mpteqb  6441  dffo3  6517  fliftfun  6704  elovmpt3rab1  7039  ordsucss  7164  tfindsg  7206  imacosupp  7486  tfrlem1  7624  tfrlem9  7633  oaordi  7779  oaordex  7791  oaass  7794  oarec  7795  omlimcl  7811  omass  7813  oen0  7819  oeordsuc  7827  nnaordi  7851  omsmolem  7886  infensuc  8293  php3  8301  suppeqfsuppbi  8444  marypha1lem  8494  hartogs  8604  card2on  8614  tz9.12lem3  8815  infxpenlem  9035  cfflb  9282  cfcoflem  9295  cfcof  9297  isf32lem12  9387  zorn2lem6  9524  ondomon  9586  alephval2  9595  pwcfsdom  9606  axrepnd  9617  fpwwe2lem12  9664  genpcd  10029  ltexprlem6  10064  recexsr  10129  axpre-sup  10191  negf1o  10661  recex  10860  zdiv  11648  uzaddcl  11945  nn01to3  11983  rpnnen1lem5  12020  rpnnen1lem5OLD  12026  xrsupsslem  12341  xrinfmsslem  12342  supxrunb1  12353  supxrunb2  12354  fz0fzelfz0  12652  fz0fzdiffz0  12655  elfzmlbp  12657  difelfzle  12659  fzo1fzo0n0  12726  elincfzoext  12733  ssfzo12bi  12770  elfznelfzo  12780  modaddmodup  12940  modfzo0difsn  12949  fsuppmapnn0fiubex  12998  seqf1o  13048  expcllem  13077  expeq0  13096  mulexp  13105  hashgt12el2  13412  hashimarni  13429  hash2prd  13458  fi1uzind  13480  swrdnd  13640  swrdswrdlem  13667  swrdswrd  13668  reuccats1  13688  swrdccat3  13700  swrdccatid  13705  repswswrd  13739  repswccat  13740  cshwidxmod  13757  2cshwcshw  13779  s4f1o  13871  wwlktovfo  13910  cjexp  14097  resqrex  14198  absexp  14251  summo  14655  fsum2d  14709  modfsummods  14731  binom  14768  clim2prod  14826  fprod2d  14917  binomfallfac  14977  efexp  15036  demoivreALT  15136  divconjdvds  15245  addmodlteqALT  15255  dfgcd2  15470  lcmfunsnlem2lem1  15558  lcmfdvdsb  15563  lcmfun  15565  coprmprod  15581  coprmproddvdslem  15582  oddprmdvds  15813  ramcl  15939  cshwsidrepswmod0  16007  cshwshashlem1  16008  ressress  16145  initoeu2lem1  16870  symggen  18096  pmtr3ncom  18101  srgmulgass  18738  srgbinom  18752  ringinvnzdiv  18800  lmodvsmmulgdi  19107  assamulgscmlem2  19563  mptcoe1fsupp  19799  coe1fzgsumdlem  19885  evl1gsumdlem  19934  psgndiflemB  20161  scmatmulcl  20541  mdetdiagid  20623  pm2mpf1  20823  mptcoe1matfsupp  20826  mp2pm2mplem4  20833  chpdmat  20865  chfacfisf  20878  chfacfisfcpmat  20879  chcoeffeq  20910  topbas  20996  fctop  21028  cctop  21030  elcls  21097  elcls3  21107  2ndcdisj  21479  filufint  21943  ovoliunlem3  23491  dvge0  23988  ulmcn  24372  gausslemma2dlem3  25313  sizusglecusg  26593  upgriswlk  26771  2pthnloop  26861  crctcshwlkn0  26948  wwlksnred  27034  wwlksnextinj  27041  wwlksnextproplem2  27052  wwlksnextproplem3  27053  usgr2wspthons3  27110  clwwlkccatlem  27136  clwlkclwwlklem2a4  27144  clwlkclwwlklem2a  27145  clwlkclwwlklem2  27147  erclwwlktr  27169  clwwlkinwwlk  27193  clwwlkf  27200  clwwlkf1  27202  wwlksext2clwwlk  27211  wwlksext2clwwlkOLD  27212  clwwlknscsh  27217  umgr2cwwk2dif  27219  erclwwlkntr  27226  clwlksfclwwlkOLD  27240  clwlksf1clwwlklemOLD  27246  clwwlknonex2  27282  uhgr3cyclex  27359  upgr4cycl4dv4e  27362  eucrctshift  27420  3cyclfrgrrn1  27464  frgrwopreglem2  27492  frgrwopreglem5  27500  frgrwopreglem5ALT  27501  numclwlk1lem2fo  27542  numclwlk2lem2f  27563  numclwlk2lem2f1o  27565  numclwlk2lem2fOLD  27570  numclwlk2lem2f1oOLD  27572  frgrreg  27587  friendshipgt3  27591  friendship  27592  grpoinvf  27720  nmosetre  27953  ipasslem1  28020  shmodsi  28582  elspansn5  28767  normcan  28769  h1datomi  28774  nmopsetretALT  29056  nmfnsetre  29070  pjss2coi  29357  pj3cor1i  29402  mdexchi  29528  superpos  29547  atcvat4i  29590  mdsymlem3  29598  mdsymlem4  29599  sumdmdii  29608  cdj3lem2b  29630  elabreximd  29680  iuninc  29711  iundisjf  29734  xrsmulgzz  30012  gsumle  30113  gsumvsca1  30116  gsumvsca2  30117  ofldchr  30148  locfinreflem  30241  xrge0iifiso  30315  lmxrge0  30332  esumfzf  30465  sigaclfu2  30518  eulerpartlemgh  30774  signstfvneq0  30983  signstfvc  30985  bccolsum  31957  faclimlem1  31961  dftrpred3g  32063  nosupbnd1  32191  nosupbnd2  32193  segletr  32552  segleantisym  32553  outsideoftr  32567  exp5d  32627  elicc3  32642  finxpreclem2  33557  wl-sbcom2d  33671  poimirlem26  33761  mblfinlem3  33774  itg2addnc  33789  indexa  33853  ax12indalem  34746  ax12inda2ALT  34747  cvrat4  35244  elpaddn0  35601  paddasslem5  35625  paddasslem14  35634  eldioph2  37844  pell1234qrdich  37944  gneispb  38948  rexlimd3  39849  rexlimdva2  39853  dffo3f  39878  rnmptlb  39965  rexabslelem  40155  climsuselem1  40351  limsupubuz  40457  stoweidlem19  40747  stoweidlem20  40748  stoweidlem34  40762  wallispilem3  40795  sge0iunmpt  41146  meaiuninc3v  41212  smflimlem4  41496  smflimmpt  41530  2elfz2melfz  41846  subsubelfzo0  41854  iccpartigtl  41877  iccpartgt  41881  icceuelpartlem  41889  fargshiftf1  41895  pfxccat3  41944  lighneallem3  42042  gbowgt5  42168  mogoldbb  42191  bgoldbtbndlem3  42213  bgoldbtbndlem4  42214  bgoldbtbnd  42215  tgblthelfgott  42221  tgblthelfgottOLD  42227  upgrwlkupwlk  42239  2zrngagrp  42461  rhmsubcrngclem2  42546  nzerooringczr  42590  lmodvsmdi  42681  ply1mulgsumlem1  42692  islindeps2  42790  elfzolborelfzop1  42827  nnolog2flm1  42902  nn0sumshdiglemA  42931
  Copyright terms: Public domain W3C validator