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

Theorem expimpd 626
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 448 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 445 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 195  df-an 384
This theorem is referenced by:  ornld  937  ralrimdva  2951  disjiun  4567  reusv3  4797  ralxfrdOLD  4801  euotd  4891  swopo  4959  wereu2  5025  poirr2  5426  sossfld  5485  oneqmini  5679  suctr  5711  elpreima  6230  fmptco  6288  isofrlem  6468  onmindif2  6881  frxp  7151  fnse  7158  suppss  7189  tposfo2  7239  wfr3g  7277  tz7.48-2  7401  omeulem1  7526  omeu  7529  nnaordex  7582  pssnn  8040  fodomfib  8102  dffi3  8197  supmo  8218  supnub  8228  infglb  8256  infnlb  8258  infmo  8261  cantnfle  8428  cantnflem1  8446  epfrs  8467  alephord2i  8760  cardinfima  8780  aceq3lem  8803  dfac2  8813  dfac12lem2  8826  axdc2lem  9130  ttukeylem6  9196  alephval2  9250  fpwwe2lem12  9319  fpwwe2lem13  9320  prlem934  9711  reclem4pr  9728  suplem1pr  9730  letr  9982  sup2  10828  uzind  11301  ledivge1le  11733  xrletr  11824  xltnegi  11880  xlemul1a  11947  ixxssixx  12016  difreicc  12131  flval3  12433  fsequb  12591  seqf1olem1  12657  expnegz  12711  hash2prd  13064  ccatrcl1  13175  relexprelg  13572  shftlem  13602  rexuzre  13886  cau3lem  13888  caubnd2  13891  caubnd  13892  climrlim2  14072  climuni  14077  2clim  14097  o1co  14111  rlimno1  14178  climbdd  14196  caurcvg  14201  summolem2  14240  summo  14241  zsum  14242  fsumf1o  14247  fsumss  14249  fsumcl2lem  14255  fsumadd  14263  fsummulc2  14304  fsumconst  14310  fsumrelem  14326  prodmolem2  14450  prodmo  14451  zprod  14452  fprodf1o  14461  fprodss  14463  fprodcl2lem  14465  fprodmul  14475  fproddiv  14476  fprodconst  14493  fprodn0  14494  dfgcd2  15047  coprmproddvdslem  15160  cncongrprm  15221  prmpwdvds  15392  infpnlem1  15398  1arith  15415  vdwapun  15462  vdwlem11  15479  vdwnnlem2  15484  ramz  15513  ramcl  15517  prmlem0  15596  firest  15862  catpropd  16138  initoid  16424  termoid  16425  initoeu2lem1  16433  pltnle  16735  pltletr  16740  pospo  16742  psss  16983  isgrpid2  17227  f1omvdco2  17637  pgpfi  17789  frgpnabllem1  18045  gsumval3eu  18074  gsumzres  18079  gsumzcl2  18080  gsumzf1o  18082  gsumzaddlem  18090  gsumconst  18103  gsumzmhm  18106  gsumzoppg  18113  ablfaclem3  18255  dvdsrtr  18421  dvdsrmul1  18422  unitgrp  18436  lspsolvlem  18909  domnmuln0  19065  gsummoncoe1  19441  pf1ind  19486  gsumfsum  19578  obslbs  19835  dmatscmcl  20070  scmatmulcl  20085  smatvscl  20091  mdetdiaglem  20165  cpmatinvcl  20283  mp2pm2mplem4  20375  cpmadugsumlemF  20442  eltg3  20519  tgidm  20537  neindisj  20673  tgrest  20715  restcld  20728  tgcn  20808  lmcnp  20860  iunconlem  20982  2ndcredom  21005  2ndc1stc  21006  1stcrest  21008  2ndcrest  21009  2ndcdisj  21011  nllyrest  21041  nllyidm  21044  lfinpfin  21079  locfincmp  21081  ptpjpre1  21126  ptuni2  21131  ptbasin  21132  ptbasfi  21136  txbasval  21161  ptpjopn  21167  ptclsg  21170  dfac14lem  21172  xkoccn  21174  txcnp  21175  ptcnplem  21176  ptcnp  21177  txtube  21195  txcmplem1  21196  txcmplem2  21197  tx2ndc  21206  txkgen  21207  xkoco1cn  21212  xkoco2cn  21213  xkococnlem  21214  xkococn  21215  xkoinjcn  21242  qtoprest  21272  kqsat  21286  kqcldsat  21288  isfild  21414  fbunfip  21425  fgabs  21435  filcon  21439  fbasrn  21440  filufint  21476  elfm2  21504  elfm3  21506  fmfnfm  21514  hausflimi  21536  cnpflfi  21555  ptcmplem2  21609  tmdgsum2  21652  cldsubg  21666  qustgpopn  21675  ustfilxp  21768  bldisj  21954  xbln0  21970  blssps  21980  blss  21981  blssexps  21982  blssex  21983  blcls  22062  metcnp3  22096  icccmplem2  22366  cnheibor  22493  iscau4  22803  ovolshftlem2  23002  ovolicc2lem5  23013  dyadmax  23089  mbfi1fseqlem4  23208  mbfi1flimlem  23212  lhop1lem  23497  dvfsumrlim  23515  aalioulem3  23810  ulmcn  23874  radcnvlt1  23893  pilem2  23927  efopn  24121  cxpeq0  24141  cxpmul2z  24154  cxpcn3lem  24205  xrlimcnp  24412  vmappw  24559  fsumvma  24655  dchrptlem1  24706  lgsqr  24793  lgsdchrval  24796  2lgslem3  24846  2sqlem6  24865  2sqlem7  24866  pntlem3  25015  pntleml  25017  brbtwn  25497  brcgr  25498  axcontlem8  25569  cusgrafilem2  25774  redwlk  25902  4cycl4dv  25961  cusconngra  25970  usg2wlkeq  26002  usg2spthonot  26181  usg2spthonot0  26182  frg2woteq  26353  pjhthmo  27351  spansncvi  27701  nmcexi  28075  cnlnssadj  28129  leopmuli  28182  elpjrn  28239  mdsl0  28359  sumdmdii  28464  fmptcof2  28645  suppss3  28696  lmxrge0  29132  bnj594  30042  bnj849  30055  erdszelem7  30239  sconpi1  30281  cvmsval  30308  cvmopnlem  30320  cvmfolem  30321  cvmliftmolem2  30324  cvmlift2lem10  30354  cvmlift2lem12  30356  cvmlift3lem5  30365  cvmlift3lem8  30368  trpredrec  30788  frr3g  30829  sltval2  30859  linethru  31236  opnrebl2  31292  neibastop2lem  31331  neibastop2  31332  bj-ssbequ1  31639  bj-cbv3ta  31703  phpreu  32359  finixpnum  32360  matunitlindflem1  32371  ptrecube  32375  poimirlem26  32401  poimirlem27  32402  poimirlem31  32406  poimir  32408  heicant  32410  voliunnfl  32419  volsupnfl  32420  itg2addnclem  32427  unirep  32473  sdclem2  32504  istotbnd3  32536  ssbnd  32553  lshpdisj  33088  lsatn0  33100  lsat0cv  33134  cvrletrN  33374  cvrval4N  33514  lncvrelatN  33881  paddasslem14  33933  paddasslem15  33934  paddasslem16  33935  pmapjoin  33952  dihglblem2N  35397  dochvalr  35460  incssnn0  36088  eldioph4b  36189  diophren  36191  fphpdo  36195  rencldnfilem  36198  pellexlem5  36211  pell1234qrne0  36231  pell1234qrmulcl  36233  pell14qrgt0  36237  pell1234qrdich  36239  pell14qrdich  36247  pell1qrge1  36248  pell1qrgap  36252  pellfundre  36259  pellfundlb  36262  dvdsacongtr  36365  jm2.19lem4  36373  aomclem4  36441  hbtlem2  36509  hbtlem4  36511  hbtlem6  36514  clcnvlem  36745  ordpss  37472  fmtnofac2lem  39816  opoeALTV  39930  opeoALTV  39931  gboage9  39984  nbumgrvtx  40563  cusgrfilem2  40667  1loopgrnb0  40712  uspgr2wlkeq  40849  upgrwlkdvdelem  40937  uspgrn2crct  41006  0enwwlksnge1  41055  usgr2wspthons3  41162  frgr2wwlkeqm  41491  av-frgrareggt1  41542  av-frgrareg  41543  nzerooringczr  41859  ellcoellss  42013  nn0sumshdiglem1  42208
  Copyright terms: Public domain W3C validator