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

Theorem expimpd 457
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 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 414 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ornld  1062  3impia  1119  ralrimdva  3113  disjiun  5057  reusv3  5315  euotd  5413  swopo  5497  wereu2  5566  poirr2  6007  sossfld  6067  reuop  6174  frpomin  6215  oneqmini  6285  suctr  6317  elpreima  6900  fmptco  6966  isofrlem  7171  onmindif2  7613  frxp  7917  fnse  7924  suppss  7960  suppssOLD  7961  tposfo2  8015  wfr3g  8077  tz7.48-2  8202  omeulem1  8334  omeu  8337  nnaordex  8390  pssnn  8872  pssnnOLD  8925  fodomfib  8980  dffi3  9077  supmo  9098  supnub  9108  infglb  9136  infnlb  9138  infmo  9141  infsupprpr  9150  cantnfle  9316  cantnflem1  9334  trpredrec  9372  epfrs  9377  frr3g  9402  updjud  9580  alephord2i  9721  cardinfima  9741  aceq3lem  9764  dfac2b  9774  dfac12lem2  9788  axdc2lem  10092  ttukeylem6  10158  alephval2  10216  fpwwe2lem11  10285  fpwwe2lem12  10286  prlem934  10677  reclem4pr  10694  suplem1pr  10696  letr  10956  sup2  11818  uzind  12299  ledivge1le  12687  xrletr  12778  xltnegi  12836  xlemul1a  12908  ixxssixx  12979  difreicc  13102  flval3  13420  fsequb  13580  seqf1olem1  13647  expnegz  13702  hash2prd  14074  ccatrcl1  14184  relexprelg  14634  shftlem  14664  rexuzre  14949  cau3lem  14951  caubnd2  14954  caubnd  14955  climrlim2  15141  climuni  15146  2clim  15166  o1co  15180  rlimno1  15250  climbdd  15268  caurcvg  15273  summolem2  15313  summo  15314  zsum  15315  fsumf1o  15320  fsumss  15322  fsumcl2lem  15328  fsumadd  15337  fsummulc2  15381  fsumconst  15387  fsumrelem  15404  prodmolem2  15530  prodmo  15531  zprod  15532  fprodf1o  15541  fprodss  15543  fprodcl2lem  15545  fprodmul  15555  fproddiv  15556  fprodconst  15573  fprodn0  15574  dfgcd2  16139  lcmfunsnlem2  16230  coprmproddvdslem  16252  cncongrprm  16318  prmpwdvds  16490  infpnlem1  16496  1arith  16513  vdwapun  16560  vdwlem11  16577  vdwnnlem2  16582  ramz  16611  ramcl  16615  prmlem0  16692  firest  16970  catpropd  17245  initoid  17540  termoid  17541  initoeu2lem1  17553  pltnle  17877  pltletr  17882  pospo  17884  psss  18119  isgrpid2  18437  f1omvdco2  18873  pgpfi  19027  frgpnabllem1  19291  gsumval3eu  19322  gsumzres  19327  gsumzcl2  19328  gsumzf1o  19330  gsumzaddlem  19339  gsumconst  19352  gsumzmhm  19355  gsumzoppg  19362  ablfaclem3  19507  dvdsrtr  19703  dvdsrmul1  19704  unitgrp  19718  lspsolvlem  20212  domnmuln0  20369  gsumfsum  20463  obslbs  20725  gsummoncoe1  21257  pf1ind  21303  dmatscmcl  21432  scmatmulcl  21447  smatvscl  21453  mdetdiaglem  21527  cpmatinvcl  21646  mp2pm2mplem4  21738  cpmadugsumlemF  21805  eltg3  21891  tgidm  21909  neindisj  22046  tgrest  22088  restcld  22101  tgcn  22181  lmcnp  22233  iunconnlem  22356  2ndcredom  22379  2ndc1stc  22380  1stcrest  22382  2ndcrest  22383  2ndcdisj  22385  nllyrest  22415  nllyidm  22418  lfinpfin  22453  locfincmp  22455  ptpjpre1  22500  ptuni2  22505  ptbasin  22506  ptbasfi  22510  txbasval  22535  ptpjopn  22541  ptclsg  22544  dfac14lem  22546  xkoccn  22548  txcnp  22549  ptcnplem  22550  ptcnp  22551  txtube  22569  txcmplem1  22570  txcmplem2  22571  tx2ndc  22580  txkgen  22581  xkoco1cn  22586  xkoco2cn  22587  xkococnlem  22588  xkococn  22589  xkoinjcn  22616  qtoprest  22646  kqsat  22660  kqcldsat  22662  isfild  22787  fbunfip  22798  fgabs  22808  filconn  22812  fbasrn  22813  filufint  22849  elfm2  22877  elfm3  22879  fmfnfm  22887  hausflimi  22909  cnpflfi  22928  ptcmplem2  22982  tmdgsum2  23025  cldsubg  23040  qustgpopn  23049  ustfilxp  23142  bldisj  23328  xbln0  23344  blssps  23354  blss  23355  blssexps  23356  blssex  23357  blcls  23436  metcnp3  23470  icccmplem2  23752  cnheibor  23884  iscau4  24208  cmssmscld  24279  ovolshftlem2  24439  ovolicc2lem5  24450  dyadmax  24527  mbfi1fseqlem4  24648  mbfi1flimlem  24652  lhop1lem  24942  dvfsumrlim  24960  aalioulem3  25259  ulmcn  25323  radcnvlt1  25342  pilem2  25376  efopn  25578  cxpeq0  25598  cxpmul2z  25611  cxpcn3lem  25665  xrlimcnp  25883  vmappw  26030  fsumvma  26126  dchrptlem1  26177  lgsqr  26264  lgsdchrval  26267  2lgslem3  26317  2sqlem6  26336  2sqlem7  26337  2sqreultlem  26360  2sqreunnltlem  26363  pntlem3  26522  pntleml  26524  brbtwn  27022  brcgr  27023  axcontlem8  27094  nbumgrvtx  27466  cusgrfilem2  27576  1loopgrnb0  27622  uspgr2wlkeq  27765  wlklenvclwlk  27774  upgrwlkdvdelem  27855  uspgrn2crct  27924  0enwwlksnge1  27980  usgr2wspthons3  28080  clwwlkccatlem  28104  clwlkclwwlkf  28123  clwwlknonel  28210  frgrncvvdeqlem9  28422  frgr2wwlkeqm  28446  frgrreggt1  28508  frgrreg  28509  pjhthmo  29415  spansncvi  29765  nmcexi  30139  cnlnssadj  30193  leopmuli  30246  elpjrn  30303  mdsl0  30423  sumdmdii  30528  fmptcof2  30746  suppss3  30811  lmxrge0  31648  bnj594  32636  bnj849  32649  subgrwlk  32838  erdszelem7  32903  sconnpi1  32945  cvmsval  32972  cvmopnlem  32984  cvmfolem  32985  cvmliftmolem2  32988  cvmlift2lem10  33018  cvmlift2lem12  33020  cvmlift3lem5  33029  cvmlift3lem8  33032  satfv0  33064  satfv1  33069  satfvsucsuc  33071  satffunlem1lem2  33109  satffunlem2lem2  33112  eldifsucnn  33441  sotr3  33483  sltval2  33630  nosupno  33677  nosupbnd1lem5  33686  noinfno  33692  sletr  33732  madebdayim  33841  sltlpss  33858  linethru  34226  opnrebl2  34281  neibastop2lem  34320  neibastop2  34321  bj-cbv3ta  34739  isinf2  35350  phpreu  35535  finixpnum  35536  lindsadd  35544  matunitlindflem1  35547  ptrecube  35551  poimirlem26  35577  poimirlem27  35578  poimirlem31  35582  poimir  35584  heicant  35586  voliunnfl  35595  volsupnfl  35596  itg2addnclem  35602  unirep  35645  sdclem2  35674  istotbnd3  35703  ssbnd  35720  lshpdisj  36775  lsatn0  36787  lsat0cv  36821  cvrletrN  37061  cvrval4N  37202  lncvrelatN  37569  paddasslem14  37621  paddasslem15  37622  paddasslem16  37623  pmapjoin  37640  dihglblem2N  39082  dochvalr  39145  sn-negex12  40154  sn-sup2  40195  prjspner1  40219  flt4lem7  40247  incssnn0  40284  eldioph4b  40384  diophren  40386  fphpdo  40390  rencldnfilem  40393  pellexlem5  40406  pell1234qrne0  40426  pell1234qrmulcl  40428  pell14qrgt0  40432  pell1234qrdich  40434  pell14qrdich  40442  pell1qrge1  40443  pell1qrgap  40447  pellfundre  40454  pellfundlb  40457  dvdsacongtr  40557  jm2.19lem4  40565  aomclem4  40633  hbtlem2  40700  hbtlem4  40702  hbtlem6  40705  harval3  40876  clcnvlem  40955  ordpss  41790  cfsetsnfsetfo  44272  euoreqb  44319  2reu8i  44323  sprsymrelf1lem  44662  sprsymrelfolem2  44664  reupr  44693  fmtnofac2lem  44739  opoeALTV  44854  opeoALTV  44855  fpprwpprb  44911  gboge9  44935  nzerooringczr  45349  ellcoellss  45495  nn0sumshdiglem1  45686  itschlc0xyqsol  45832  itsclc0  45836  opnneilv  45921
  Copyright terms: Public domain W3C validator