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

Theorem expimpd 445
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expimpd.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
expimpd (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 401 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 398 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 198  df-an 385
This theorem is referenced by:  ornld  1084  3impia  1145  ralrimdva  3116  disjiun  4799  reusv3  5042  euotd  5136  swopo  5210  wereu2  5276  poirr2  5705  sossfld  5765  oneqmini  5961  suctr  5993  elpreima  6529  fmptco  6589  isofrlem  6784  onmindif2  7212  frxp  7491  fnse  7498  suppss  7530  tposfo2  7580  wfr3g  7618  tz7.48-2  7743  omeulem1  7869  omeu  7872  nnaordex  7925  pssnn  8387  fodomfib  8449  dffi3  8546  supmo  8567  supnub  8577  infglb  8605  infnlb  8607  infmo  8610  cantnfle  8785  cantnflem1  8803  epfrs  8824  updjud  9013  alephord2i  9153  cardinfima  9173  aceq3lem  9196  dfac2b  9206  dfac2OLD  9208  dfac12lem2  9221  axdc2lem  9525  ttukeylem6  9591  alephval2  9649  fpwwe2lem12  9718  fpwwe2lem13  9719  prlem934  10110  reclem4pr  10127  suplem1pr  10129  letr  10387  sup2  11235  uzind  11719  ledivge1le  12102  xrletr  12194  xltnegi  12252  xlemul1a  12323  ixxssixx  12394  difreicc  12514  flval3  12827  fsequb  12985  seqf1olem1  13050  expnegz  13104  hash2prd  13461  ccatrcl1  13568  relexprelg  14066  shftlem  14096  rexuzre  14380  cau3lem  14382  caubnd2  14385  caubnd  14386  climrlim2  14566  climuni  14571  2clim  14591  o1co  14605  rlimno1  14672  climbdd  14690  caurcvg  14695  summolem2  14735  summo  14736  zsum  14737  fsumf1o  14742  fsumss  14744  fsumcl2lem  14750  fsumadd  14758  fsummulc2  14803  fsumconst  14809  fsumrelem  14826  prodmolem2  14951  prodmo  14952  zprod  14953  fprodf1o  14962  fprodss  14964  fprodcl2lem  14966  fprodmul  14976  fproddiv  14977  fprodconst  14994  fprodn0  14995  dfgcd2  15547  coprmproddvdslem  15659  cncongrprm  15719  prmpwdvds  15890  infpnlem1  15896  1arith  15913  vdwapun  15960  vdwlem11  15977  vdwnnlem2  15982  ramz  16011  ramcl  16015  prmlem0  16089  firest  16362  catpropd  16637  initoid  16923  termoid  16924  initoeu2lem1  16932  pltnle  17235  pltletr  17240  pospo  17242  psss  17483  isgrpid2  17728  f1omvdco2  18134  pgpfi  18287  frgpnabllem1  18545  gsumval3eu  18574  gsumzres  18579  gsumzcl2  18580  gsumzf1o  18582  gsumzaddlem  18590  gsumconst  18603  gsumzmhm  18606  gsumzoppg  18613  ablfaclem3  18756  dvdsrtr  18922  dvdsrmul1  18923  unitgrp  18937  lspsolvlem  19418  domnmuln0  19575  gsummoncoe1  19950  pf1ind  19995  gsumfsum  20089  obslbs  20353  dmatscmcl  20589  scmatmulcl  20604  smatvscl  20610  mdetdiaglem  20684  cpmatinvcl  20804  mp2pm2mplem4  20896  cpmadugsumlemF  20963  eltg3  21049  tgidm  21067  neindisj  21204  tgrest  21246  restcld  21259  tgcn  21339  lmcnp  21391  iunconnlem  21513  2ndcredom  21536  2ndc1stc  21537  1stcrest  21539  2ndcrest  21540  2ndcdisj  21542  nllyrest  21572  nllyidm  21575  lfinpfin  21610  locfincmp  21612  ptpjpre1  21657  ptuni2  21662  ptbasin  21663  ptbasfi  21667  txbasval  21692  ptpjopn  21698  ptclsg  21701  dfac14lem  21703  xkoccn  21705  txcnp  21706  ptcnplem  21707  ptcnp  21708  txtube  21726  txcmplem1  21727  txcmplem2  21728  tx2ndc  21737  txkgen  21738  xkoco1cn  21743  xkoco2cn  21744  xkococnlem  21745  xkococn  21746  xkoinjcn  21773  qtoprest  21803  kqsat  21817  kqcldsat  21819  isfild  21944  fbunfip  21955  fgabs  21965  filconn  21969  fbasrn  21970  filufint  22006  elfm2  22034  elfm3  22036  fmfnfm  22044  hausflimi  22066  cnpflfi  22085  ptcmplem2  22139  tmdgsum2  22182  cldsubg  22196  qustgpopn  22205  ustfilxp  22298  bldisj  22485  xbln0  22501  blssps  22511  blss  22512  blssexps  22513  blssex  22514  blcls  22593  metcnp3  22627  icccmplem2  22908  cnheibor  23036  iscau4  23359  cmssmscld  23430  ovolshftlem2  23571  ovolicc2lem5  23582  dyadmax  23659  mbfi1fseqlem4  23779  mbfi1flimlem  23783  lhop1lem  24070  dvfsumrlim  24088  aalioulem3  24383  ulmcn  24447  radcnvlt1  24466  pilem2  24500  efopn  24698  cxpeq0  24718  cxpmul2z  24731  cxpcn3lem  24782  xrlimcnp  24989  vmappw  25136  fsumvma  25232  dchrptlem1  25283  lgsqr  25370  lgsdchrval  25373  2lgslem3  25423  2sqlem6  25442  2sqlem7  25443  pntlem3  25592  pntleml  25594  brbtwn  26073  brcgr  26074  axcontlem8  26145  nbumgrvtx  26524  cusgrfilem2  26646  1loopgrnb0  26692  uspgr2wlkeq  26836  upgrwlkdvdelem  26927  uspgrn2crct  26996  0enwwlksnge1  27058  usgr2wspthons3  27192  clwwlkccatlem  27219  clwlkclwwlkfOLD  27242  clwlkclwwlkf  27246  clwwlknonel  27370  frgrncvvdeqlem9  27590  frgr2wwlkeqm  27614  frgrreggt1  27712  frgrreg  27713  pjhthmo  28620  spansncvi  28970  nmcexi  29344  cnlnssadj  29398  leopmuli  29451  elpjrn  29508  mdsl0  29628  sumdmdii  29733  fmptcof2  29910  suppss3  29954  lmxrge0  30448  bnj594  31433  bnj849  31446  erdszelem7  31630  sconnpi1  31672  cvmsval  31699  cvmopnlem  31711  cvmfolem  31712  cvmliftmolem2  31715  cvmlift2lem10  31745  cvmlift2lem12  31747  cvmlift3lem5  31756  cvmlift3lem8  31759  sotr3  32104  trpredrec  32184  frpomin  32185  frr3g  32226  sltval2  32256  nosupno  32296  nosupbnd1lem5  32305  sletr  32330  linethru  32707  opnrebl2  32762  neibastop2lem  32801  neibastop2  32802  bj-ssbequ1  33083  bj-cbv3ta  33148  bj-ismoored  33493  phpreu  33820  finixpnum  33821  matunitlindflem1  33832  ptrecube  33836  poimirlem26  33862  poimirlem27  33863  poimirlem31  33867  poimir  33869  heicant  33871  voliunnfl  33880  volsupnfl  33881  itg2addnclem  33887  unirep  33933  sdclem2  33963  istotbnd3  33995  ssbnd  34012  lshpdisj  34946  lsatn0  34958  lsat0cv  34992  cvrletrN  35232  cvrval4N  35373  lncvrelatN  35740  paddasslem14  35792  paddasslem15  35793  paddasslem16  35794  pmapjoin  35811  dihglblem2N  37253  dochvalr  37316  incssnn0  37955  eldioph4b  38056  diophren  38058  fphpdo  38062  rencldnfilem  38065  pellexlem5  38078  pell1234qrne0  38098  pell1234qrmulcl  38100  pell14qrgt0  38104  pell1234qrdich  38106  pell14qrdich  38114  pell1qrge1  38115  pell1qrgap  38119  pellfundre  38126  pellfundlb  38129  dvdsacongtr  38231  jm2.19lem4  38239  aomclem4  38307  hbtlem2  38374  hbtlem4  38376  hbtlem6  38379  clcnvlem  38608  ordpss  39330  fmtnofac2lem  42159  opoeALTV  42273  opeoALTV  42274  gboge9  42331  sprsymrelf1lem  42413  sprsymrelfolem2  42415  nzerooringczr  42744  ellcoellss  42896  nn0sumshdiglem1  43087
  Copyright terms: Public domain W3C validator