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

Theorem expimpd 454
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 413 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 411 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ornld  1055  3impia  1111  ralrimdva  3193  disjiun  5049  reusv3  5301  euotd  5399  swopo  5482  wereu2  5550  poirr2  5981  sossfld  6040  reuop  6141  oneqmini  6239  suctr  6271  elpreima  6823  fmptco  6886  isofrlem  7088  onmindif2  7518  frxp  7814  fnse  7821  suppss  7854  tposfo2  7909  wfr3g  7947  tz7.48-2  8072  omeulem1  8201  omeu  8204  nnaordex  8257  pssnn  8728  fodomfib  8790  dffi3  8887  supmo  8908  supnub  8918  infglb  8946  infnlb  8948  infmo  8951  infsupprpr  8960  cantnfle  9126  cantnflem1  9144  epfrs  9165  updjud  9355  alephord2i  9495  cardinfima  9515  aceq3lem  9538  dfac2b  9548  dfac12lem2  9562  axdc2lem  9862  ttukeylem6  9928  alephval2  9986  fpwwe2lem12  10055  fpwwe2lem13  10056  prlem934  10447  reclem4pr  10464  suplem1pr  10466  letr  10726  sup2  11589  uzind  12066  ledivge1le  12453  xrletr  12544  xltnegi  12602  xlemul1a  12674  ixxssixx  12745  difreicc  12863  flval3  13178  fsequb  13336  seqf1olem1  13402  expnegz  13456  hash2prd  13826  ccatrcl1  13941  relexprelg  14390  shftlem  14420  rexuzre  14705  cau3lem  14707  caubnd2  14710  caubnd  14711  climrlim2  14897  climuni  14902  2clim  14922  o1co  14936  rlimno1  15003  climbdd  15021  caurcvg  15026  summolem2  15065  summo  15066  zsum  15067  fsumf1o  15072  fsumss  15074  fsumcl2lem  15080  fsumadd  15088  fsummulc2  15131  fsumconst  15137  fsumrelem  15154  prodmolem2  15281  prodmo  15282  zprod  15283  fprodf1o  15292  fprodss  15294  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodconst  15324  fprodn0  15325  dfgcd2  15886  lcmfunsnlem2  15976  coprmproddvdslem  15998  cncongrprm  16061  prmpwdvds  16232  infpnlem1  16238  1arith  16255  vdwapun  16302  vdwlem11  16319  vdwnnlem2  16324  ramz  16353  ramcl  16357  prmlem0  16431  firest  16698  catpropd  16971  initoid  17257  termoid  17258  initoeu2lem1  17266  pltnle  17568  pltletr  17573  pospo  17575  psss  17816  isgrpid2  18072  f1omvdco2  18498  pgpfi  18652  frgpnabllem1  18915  gsumval3eu  18946  gsumzres  18951  gsumzcl2  18952  gsumzf1o  18954  gsumzaddlem  18963  gsumconst  18976  gsumzmhm  18979  gsumzoppg  18986  ablfaclem3  19131  dvdsrtr  19324  dvdsrmul1  19325  unitgrp  19339  lspsolvlem  19836  domnmuln0  19992  gsummoncoe1  20391  pf1ind  20436  gsumfsum  20530  obslbs  20792  dmatscmcl  21030  scmatmulcl  21045  smatvscl  21051  mdetdiaglem  21125  cpmatinvcl  21243  mp2pm2mplem4  21335  cpmadugsumlemF  21402  eltg3  21488  tgidm  21506  neindisj  21643  tgrest  21685  restcld  21698  tgcn  21778  lmcnp  21830  iunconnlem  21953  2ndcredom  21976  2ndc1stc  21977  1stcrest  21979  2ndcrest  21980  2ndcdisj  21982  nllyrest  22012  nllyidm  22015  lfinpfin  22050  locfincmp  22052  ptpjpre1  22097  ptuni2  22102  ptbasin  22103  ptbasfi  22107  txbasval  22132  ptpjopn  22138  ptclsg  22141  dfac14lem  22143  xkoccn  22145  txcnp  22146  ptcnplem  22147  ptcnp  22148  txtube  22166  txcmplem1  22167  txcmplem2  22168  tx2ndc  22177  txkgen  22178  xkoco1cn  22183  xkoco2cn  22184  xkococnlem  22185  xkococn  22186  xkoinjcn  22213  qtoprest  22243  kqsat  22257  kqcldsat  22259  isfild  22384  fbunfip  22395  fgabs  22405  filconn  22409  fbasrn  22410  filufint  22446  elfm2  22474  elfm3  22476  fmfnfm  22484  hausflimi  22506  cnpflfi  22525  ptcmplem2  22579  tmdgsum2  22622  cldsubg  22636  qustgpopn  22645  ustfilxp  22738  bldisj  22925  xbln0  22941  blssps  22951  blss  22952  blssexps  22953  blssex  22954  blcls  23033  metcnp3  23067  icccmplem2  23348  cnheibor  23476  iscau4  23799  cmssmscld  23870  ovolshftlem2  24028  ovolicc2lem5  24039  dyadmax  24116  mbfi1fseqlem4  24236  mbfi1flimlem  24240  lhop1lem  24527  dvfsumrlim  24545  aalioulem3  24840  ulmcn  24904  radcnvlt1  24923  pilem2  24957  efopn  25156  cxpeq0  25176  cxpmul2z  25189  cxpcn3lem  25243  xrlimcnp  25462  vmappw  25609  fsumvma  25705  dchrptlem1  25756  lgsqr  25843  lgsdchrval  25846  2lgslem3  25896  2sqlem6  25915  2sqlem7  25916  2sqreultlem  25939  2sqreunnltlem  25942  pntlem3  26101  pntleml  26103  brbtwn  26601  brcgr  26602  axcontlem8  26673  nbumgrvtx  27044  cusgrfilem2  27154  1loopgrnb0  27200  uspgr2wlkeq  27343  wlklenvclwlk  27352  upgrwlkdvdelem  27433  uspgrn2crct  27502  0enwwlksnge1  27558  usgr2wspthons3  27659  clwwlkccatlem  27683  clwlkclwwlkf  27702  clwwlknonel  27790  frgrncvvdeqlem9  28002  frgr2wwlkeqm  28026  frgrreggt1  28088  frgrreg  28089  pjhthmo  28995  spansncvi  29345  nmcexi  29719  cnlnssadj  29773  leopmuli  29826  elpjrn  29883  mdsl0  30003  sumdmdii  30108  fmptcof2  30319  suppss3  30375  lmxrge0  31083  bnj594  32072  bnj849  32085  subgrwlk  32265  erdszelem7  32330  sconnpi1  32372  cvmsval  32399  cvmopnlem  32411  cvmfolem  32412  cvmliftmolem2  32415  cvmlift2lem10  32445  cvmlift2lem12  32447  cvmlift3lem5  32456  cvmlift3lem8  32459  satfv0  32491  satfv1  32496  satfvsucsuc  32498  satffunlem1lem2  32536  satffunlem2lem2  32539  sotr3  32888  trpredrec  32963  frpomin  32964  frr3g  33007  sltval2  33049  nosupno  33089  nosupbnd1lem5  33098  sletr  33123  linethru  33500  opnrebl2  33555  neibastop2lem  33594  neibastop2  33595  bj-cbv3ta  33994  isinf2  34557  phpreu  34745  finixpnum  34746  lindsadd  34754  matunitlindflem1  34757  ptrecube  34761  poimirlem26  34787  poimirlem27  34788  poimirlem31  34792  poimir  34794  heicant  34796  voliunnfl  34805  volsupnfl  34806  itg2addnclem  34812  unirep  34858  sdclem2  34887  istotbnd3  34919  ssbnd  34936  lshpdisj  35992  lsatn0  36004  lsat0cv  36038  cvrletrN  36278  cvrval4N  36419  lncvrelatN  36786  paddasslem14  36838  paddasslem15  36839  paddasslem16  36840  pmapjoin  36857  dihglblem2N  38299  dochvalr  38362  incssnn0  39175  eldioph4b  39275  diophren  39277  fphpdo  39281  rencldnfilem  39284  pellexlem5  39297  pell1234qrne0  39317  pell1234qrmulcl  39319  pell14qrgt0  39323  pell1234qrdich  39325  pell14qrdich  39333  pell1qrge1  39334  pell1qrgap  39338  pellfundre  39345  pellfundlb  39348  dvdsacongtr  39448  jm2.19lem4  39456  aomclem4  39524  hbtlem2  39591  hbtlem4  39593  hbtlem6  39596  harval3  39771  clcnvlem  39850  ordpss  40650  euoreqb  43176  2reu8i  43180  sprsymrelf1lem  43487  sprsymrelfolem2  43489  reupr  43518  fmtnofac2lem  43564  opoeALTV  43682  opeoALTV  43683  fpprwpprb  43739  gboge9  43763  nzerooringczr  44177  ellcoellss  44324  nn0sumshdiglem1  44515  itschlc0xyqsol  44588  itsclc0  44592
  Copyright terms: Public domain W3C validator