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

Theorem expimpd 628
 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 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 446 1 (𝜑 → ((𝜓𝜒) → 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  ornld  958  ralrimdva  2998  disjiun  4672  reusv3  4906  ralxfrdOLD  4910  euotd  5004  swopo  5074  wereu2  5140  poirr2  5555  sossfld  5615  oneqmini  5814  suctr  5846  elpreima  6377  fmptco  6436  isofrlem  6630  onmindif2  7054  frxp  7332  fnse  7339  suppss  7370  tposfo2  7420  wfr3g  7458  tz7.48-2  7582  omeulem1  7707  omeu  7710  nnaordex  7763  pssnn  8219  fodomfib  8281  dffi3  8378  supmo  8399  supnub  8409  infglb  8437  infnlb  8439  infmo  8442  cantnfle  8606  cantnflem1  8624  epfrs  8645  alephord2i  8938  cardinfima  8958  aceq3lem  8981  dfac2  8991  dfac12lem2  9004  axdc2lem  9308  ttukeylem6  9374  alephval2  9432  fpwwe2lem12  9501  fpwwe2lem13  9502  prlem934  9893  reclem4pr  9910  suplem1pr  9912  letr  10169  sup2  11017  uzind  11507  ledivge1le  11939  xrletr  12027  xltnegi  12085  xlemul1a  12156  ixxssixx  12227  difreicc  12342  flval3  12656  fsequb  12814  seqf1olem1  12880  expnegz  12934  hash2prd  13295  ccatrcl1  13412  relexprelg  13822  shftlem  13852  rexuzre  14136  cau3lem  14138  caubnd2  14141  caubnd  14142  climrlim2  14322  climuni  14327  2clim  14347  o1co  14361  rlimno1  14428  climbdd  14446  caurcvg  14451  summolem2  14491  summo  14492  zsum  14493  fsumf1o  14498  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumconst  14566  fsumrelem  14583  prodmolem2  14709  prodmo  14710  zprod  14711  fprodf1o  14720  fprodss  14722  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodconst  14752  fprodn0  14753  dfgcd2  15310  coprmproddvdslem  15423  cncongrprm  15484  prmpwdvds  15655  infpnlem1  15661  1arith  15678  vdwapun  15725  vdwlem11  15742  vdwnnlem2  15747  ramz  15776  ramcl  15780  prmlem0  15859  firest  16140  catpropd  16416  initoid  16702  termoid  16703  initoeu2lem1  16711  pltnle  17013  pltletr  17018  pospo  17020  psss  17261  isgrpid2  17505  f1omvdco2  17914  pgpfi  18066  frgpnabllem1  18322  gsumval3eu  18351  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  ablfaclem3  18532  dvdsrtr  18698  dvdsrmul1  18699  unitgrp  18713  lspsolvlem  19190  domnmuln0  19346  gsummoncoe1  19722  pf1ind  19767  gsumfsum  19861  obslbs  20122  dmatscmcl  20357  scmatmulcl  20372  smatvscl  20378  mdetdiaglem  20452  cpmatinvcl  20570  mp2pm2mplem4  20662  cpmadugsumlemF  20729  eltg3  20814  tgidm  20832  neindisj  20969  tgrest  21011  restcld  21024  tgcn  21104  lmcnp  21156  iunconnlem  21278  2ndcredom  21301  2ndc1stc  21302  1stcrest  21304  2ndcrest  21305  2ndcdisj  21307  nllyrest  21337  nllyidm  21340  lfinpfin  21375  locfincmp  21377  ptpjpre1  21422  ptuni2  21427  ptbasin  21428  ptbasfi  21432  txbasval  21457  ptpjopn  21463  ptclsg  21466  dfac14lem  21468  xkoccn  21470  txcnp  21471  ptcnplem  21472  ptcnp  21473  txtube  21491  txcmplem1  21492  txcmplem2  21493  tx2ndc  21502  txkgen  21503  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  xkococn  21511  xkoinjcn  21538  qtoprest  21568  kqsat  21582  kqcldsat  21584  isfild  21709  fbunfip  21720  fgabs  21730  filconn  21734  fbasrn  21735  filufint  21771  elfm2  21799  elfm3  21801  fmfnfm  21809  hausflimi  21831  cnpflfi  21850  ptcmplem2  21904  tmdgsum2  21947  cldsubg  21961  qustgpopn  21970  ustfilxp  22063  bldisj  22250  xbln0  22266  blssps  22276  blss  22277  blssexps  22278  blssex  22279  blcls  22358  metcnp3  22392  icccmplem2  22673  cnheibor  22801  iscau4  23123  ovolshftlem2  23324  ovolicc2lem5  23335  dyadmax  23412  mbfi1fseqlem4  23530  mbfi1flimlem  23534  lhop1lem  23821  dvfsumrlim  23839  aalioulem3  24134  ulmcn  24198  radcnvlt1  24217  pilem2  24251  efopn  24449  cxpeq0  24469  cxpmul2z  24482  cxpcn3lem  24533  xrlimcnp  24740  vmappw  24887  fsumvma  24983  dchrptlem1  25034  lgsqr  25121  lgsdchrval  25124  2lgslem3  25174  2sqlem6  25193  2sqlem7  25194  pntlem3  25343  pntleml  25345  brbtwn  25824  brcgr  25825  axcontlem8  25896  nbumgrvtx  26287  cusgrfilem2  26408  1loopgrnb0  26454  uspgr2wlkeq  26598  upgrwlkdvdelem  26688  uspgrn2crct  26756  0enwwlksnge1  26818  usgr2wspthons3  26931  clwwlknonel  27070  frgrncvvdeqlem9  27287  frgr2wwlkeqm  27311  clwwlkccatlem  27331  frgrreggt1  27380  frgrreg  27381  pjhthmo  28289  spansncvi  28639  nmcexi  29013  cnlnssadj  29067  leopmuli  29120  elpjrn  29177  mdsl0  29297  sumdmdii  29402  fmptcof2  29585  suppss3  29630  lmxrge0  30126  bnj594  31108  bnj849  31121  erdszelem7  31305  sconnpi1  31347  cvmsval  31374  cvmopnlem  31386  cvmfolem  31387  cvmliftmolem2  31390  cvmlift2lem10  31420  cvmlift2lem12  31422  cvmlift3lem5  31431  cvmlift3lem8  31434  sotr3  31782  trpredrec  31862  frpomin  31863  frr3g  31904  sltval2  31934  nosupno  31974  nosupbnd1lem5  31983  sletr  32008  linethru  32385  opnrebl2  32441  neibastop2lem  32480  neibastop2  32481  bj-ssbequ1  32769  bj-cbv3ta  32835  bj-ismoored  33187  phpreu  33523  finixpnum  33524  matunitlindflem1  33535  ptrecube  33539  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  poimir  33572  heicant  33574  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  unirep  33637  sdclem2  33668  istotbnd3  33700  ssbnd  33717  lshpdisj  34592  lsatn0  34604  lsat0cv  34638  cvrletrN  34878  cvrval4N  35018  lncvrelatN  35385  paddasslem14  35437  paddasslem15  35438  paddasslem16  35439  pmapjoin  35456  dihglblem2N  36900  dochvalr  36963  incssnn0  37591  eldioph4b  37692  diophren  37694  fphpdo  37698  rencldnfilem  37701  pellexlem5  37714  pell1234qrne0  37734  pell1234qrmulcl  37736  pell14qrgt0  37740  pell1234qrdich  37742  pell14qrdich  37750  pell1qrge1  37751  pell1qrgap  37755  pellfundre  37762  pellfundlb  37765  dvdsacongtr  37868  jm2.19lem4  37876  aomclem4  37944  hbtlem2  38011  hbtlem4  38013  hbtlem6  38016  clcnvlem  38247  ordpss  38972  fmtnofac2lem  41805  opoeALTV  41919  opeoALTV  41920  gboge9  41977  sprsymrelf1lem  42066  sprsymrelfolem2  42068  nzerooringczr  42397  ellcoellss  42549  nn0sumshdiglem1  42740
 Copyright terms: Public domain W3C validator