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

Theorem impr 444
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
impr.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impr ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem impr
StepHypRef Expression
1 impr.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 399 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 407 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:  reximddv2  3219  moi2  3596  preq12bg  4584  prel12gOLD  4585  disjxiun  4852  disjxun  4853  wereu2  5321  f1ocnv2d  7126  extmptsuppeq  7563  suppssr  7571  omeulem1  7909  oelim2  7922  oeoa  7924  boxriin  8197  frfi  8454  fipreima  8521  marypha1lem  8588  supiso  8630  ordtypelem10  8681  r1ordg  8898  infxpenc2lem1  9135  acndom  9167  acndom2  9170  cofsmo  9386  cfcoflem  9389  fin23lem28  9457  fin23lem36  9465  isf32lem1  9470  isf32lem2  9471  isf32lem5  9474  isf34lem4  9494  fin1a2lem6  9522  fin1a2s  9531  ttukeylem2  9627  ttukeylem6  9631  fpwwe2lem8  9754  fpwwe2lem12  9758  inar1  9892  grudomon  9934  axpre-sup  10285  prodge0OLD  11165  un0addcl  11612  un0mulcl  11613  peano2uz2  11751  rpnnen1lem2  12053  rpnnen1lem1  12054  rpnnen1lem3  12055  rpnnen1lem5  12057  xlemul1a  12356  fzadd2  12619  elfz2nn0  12674  fzind2  12830  expaddz  13147  expmulz  13149  swrdswrd  13704  swrdccatin12lem2c  13732  swrdccatin12  13735  cau3lem  14337  lo1bdd2  14498  climuni  14526  fsumcom2  14748  fprodcom2  14955  dvdsval2  15226  algcvga  15531  lcmgcdlem  15558  coprmproddvdslem  15614  divgcdcoprmex  15618  iserodd  15777  prmpwdvds  15845  ram0  15963  catpropd  16593  mrcmndind  17591  isgrpinv  17697  gicsubgen  17942  sylow2alem2  18254  sylow2a  18255  frgpuptinv  18405  ablfac1eu  18694  dvdsrcl2  18872  islss4  19189  lspsnel6  19221  lmhmima  19274  lsmcl  19310  gsumbagdiag  19605  psrass1lem  19606  coe1tmmul2  19874  psgnodpm  20161  dsmmlss  20319  islindf4  20408  gsumcom3fi  20437  dmatscmcl  20541  mdetdiaglem  20636  mdetunilem9  20658  pm2mp  20864  epttop  21048  neindisj  21156  neitr  21219  restcls  21220  restntr  21221  ordtrest2lem  21242  cncnp  21319  cnconst  21323  1stcrest  21491  2ndcdisj  21494  2ndcsep  21497  1stccnp  21500  islly2  21522  1stckgenlem  21591  ptbasin  21615  ptbasfi  21619  ptcnplem  21659  ptcnp  21660  tx1stc  21688  qtophmeo  21855  filconn  21921  filuni  21923  ufileu  21957  elfm3  21988  rnelfmlem  21990  fmfnfmlem4  21995  cnpflf2  22038  alexsubALTlem4  22088  ptcmplem3  22092  ptcmplem4  22093  ptcmplem5  22094  tsmsxplem1  22190  bl2in  22439  metcnpi  22583  metcnpi2  22584  metcnpi3  22585  recld2  22851  icoopnst  22972  iocopnst  22973  ncvs1  23190  iscfil3  23305  iscmet3lem2  23324  ovoliunlem1  23506  ovolicc2lem2  23522  ovolicc2lem4  23524  voliun  23558  volsuplem  23559  dyadmbllem  23603  mbfinf  23669  mbflimsup  23670  itg2seq  23746  itg2splitlem  23752  itg2cnlem1  23765  ellimc3  23880  dvnadd  23929  dvcnvlem  23976  c1liplem1  23996  lhop2  24015  coe1mul3  24096  ply1divex  24133  dvdsq1p  24157  aannenlem1  24320  aalioulem2  24325  dvtaylp  24361  ulmdvlem3  24393  iblulm  24398  cxpmul2z  24674  leibpilem1  24904  xrlimcnp  24932  lgambdd  25000  wilthlem2  25032  basellem3  25046  dvdsflsumcom  25151  perfect  25193  dchreq  25220  dchrsum  25231  bposlem1  25246  lgsquad2  25348  dchrisum0fno1  25437  pntibnd  25519  lmieu  25913  ax5seglem5  26050  axeuclid  26080  egrsubgr  26408  nbumgrvtx  26481  wwlksnextsur  27060  wwlksext2clwwlkOLD  27231  numclwwlk2lem1lem  27541  nmcvcn  27901  ubthlem1  28077  leopmul2i  29345  hstel2  29429  atom1d  29563  cdj1i  29643  f1o3d  29781  xrge0addge  29872  reff  30254  ordtrest2NEWlem  30316  esumcst  30473  eulerpartlemgh  30788  cvmscld  31600  frpomin  32081  cgrxfr  32505  finminlem  32655  nn0prpwlem  32660  neibastop1  32697  neibastop2lem  32698  tailfb  32715  finixpnum  33726  lindsenlbs  33736  matunitlindflem2  33738  poimirlem4  33745  poimirlem25  33766  poimirlem26  33767  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  heicant  33776  mblfinlem3  33780  mblfinlem4  33781  itg2addnclem  33792  itg2addnclem3  33794  ftc1anc  33824  subspopn  33878  prdsbnd  33922  heibor1lem  33938  heiborlem1  33940  heibor  33950  isdrngo2  34087  rngoisocnv  34110  maxidlmax  34172  riotasv3d  34758  lkrpssN  34962  intnatN  35206  elpaddatiN  35604  pexmidlem5N  35773  lhpj1  35821  ltrnu  35920  cdlemn11pre  37009  dihord2pre  37024  dih1dimatlem0  37127  lcfrlem9  37349  rexrabdioph  37878  ctbnfien  37902  irrapxlem3  37908  elpell14qr2  37946  elpell1qr2  37956  kelac1  38152  iunrelexpuztr  38529  rfovcnvfvd  38819  radcnvrat  39031  nznngen  39033  tz6.12-afv  41780  tz6.12-afv2  41847  iccelpart  41962  pfxccatin12  42018  lighneallem4  42120  perfectALTV  42225  bgoldbtbndlem3  42288  tgoldbach  42298  isassintop  42432  ellcoellss  42810  lindslinindsimp2  42838  aacllem  43136
  Copyright terms: Public domain W3C validator