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

Theorem impr 619
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
impr.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
impr  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem impr
StepHypRef Expression
1 impr.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 433 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  reximddv2  2940  moi2  3284  preq12bg  4205  prel12g  4206  disjxiun  4444  disjxun  4445  wereu2  4876  frsn  5069  suppssrOLD  6013  f1ocnv2d  6508  extmptsuppeq  6921  suppssr  6928  omeulem1  7228  oelim2  7241  oeoa  7243  boxriin  7508  frfi  7761  fipreima  7822  marypha1lem  7889  supiso  7929  ordtypelem10  7948  r1ordg  8192  infxpenc2lem1  8392  acndom  8428  acndom2  8431  cofsmo  8645  cfcoflem  8648  fin23lem28  8716  fin23lem36  8724  isf32lem1  8729  isf32lem2  8730  isf32lem5  8733  isf34lem4  8753  fin1a2lem6  8781  fin1a2s  8790  ttukeylem2  8886  ttukeylem6  8890  fpwwe2lem8  9011  fpwwe2lem12  9015  inar1  9149  grudomon  9191  axpre-sup  9542  prodge0  10385  un0addcl  10825  un0mulcl  10826  peano2uz2  10944  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  xlemul1a  11476  elfz2nn0  11764  fzind2  11888  expaddz  12172  expmulz  12174  swrdswrd  12642  swrdccatin12lem2c  12670  swrdccatin12  12673  cau3lem  13143  lo1bdd2  13303  climuni  13331  fsumcom2  13545  dvdsval2  13843  algcvga  14060  iserodd  14211  prmpwdvds  14274  ram0  14392  catpropd  14958  mrcmndind  15804  isgrpinv  15898  gicsubgen  16118  sylow2alem2  16431  sylow2a  16432  frgpuptinv  16582  ablfac1eu  16911  dvdsrcl2  17080  islss4  17388  lspsnel6  17420  lmhmima  17473  lsmcl  17509  gsumbagdiag  17796  psrass1lem  17797  coe1tmmul2  18085  psgnodpm  18388  dsmmlss  18539  islindf4  18637  gsumcom3fi  18666  dmatscmcl  18769  mdetdiaglem  18864  mdetunilem9  18886  pm2mp  19090  epttop  19273  neindisj  19381  neitr  19444  restcls  19445  restntr  19446  ordtrest2lem  19467  cncnp  19544  cnconst  19548  1stcrest  19717  2ndcdisj  19720  2ndcsep  19723  1stccnp  19726  islly2  19748  1stckgenlem  19786  ptbasin  19810  ptbasfi  19814  ptcnplem  19854  ptcnp  19855  tx1stc  19883  qtophmeo  20050  filcon  20116  filuni  20118  ufileu  20152  elfm3  20183  rnelfmlem  20185  fmfnfmlem4  20190  cnpflf2  20233  alexsubALTlem4  20282  ptcmplem3  20286  ptcmplem4  20287  ptcmplem5  20288  tsmsxplem1  20387  bl2in  20635  metcnpi  20779  metcnpi2  20780  metcnpi3  20781  recld2  21051  icoopnst  21171  iocopnst  21172  iscfil3  21444  iscmet3lem2  21463  ovoliunlem1  21645  ovolicc2lem2  21661  ovolicc2lem4  21663  voliun  21696  volsuplem  21697  dyadmbllem  21740  mbfinf  21804  mbflimsup  21805  itg2seq  21881  itg2splitlem  21887  itg2cnlem1  21900  ellimc3  22015  dvnadd  22064  dvcnvlem  22109  c1liplem1  22129  lhop2  22148  coe1mul3  22232  ply1divex  22269  dvdsq1p  22293  aannenlem1  22455  aalioulem2  22460  dvtaylp  22496  ulmdvlem3  22528  iblulm  22533  cxpmul2z  22797  leibpilem1  22996  xrlimcnp  23023  wilthlem2  23068  basellem3  23081  dvdsflsumcom  23189  perfect  23231  dchreq  23258  dchrsum  23269  bposlem1  23284  lgsquad2  23360  dchrisum0fno1  23421  pntibnd  23503  lmieu  23824  ax5seglem5  23909  axeuclid  23939  spthispth  24248  wwlkextsur  24404  wwlkext2clwwlk  24476  ghgrp  25043  ghablo  25044  nmcvcn  25278  ubthlem1  25459  leopmul2i  26727  hstel2  26811  atom1d  26945  cdj1i  27025  f1o3d  27141  ordtrest2NEWlem  27537  esumcst  27708  eulerpartlemgh  27954  lgambdd  28216  cvmscld  28355  fprodcom2  28688  nofulllem4  29039  cgrxfr  29279  finixpnum  29612  heicant  29624  mblfinlem3  29628  mblfinlem4  29629  itg2addnclem  29641  itg2addnclem3  29643  ftc1anc  29673  finminlem  29711  nn0prpwlem  29715  neibastop1  29778  neibastop2lem  29779  tailfb  29796  fzadd2  29835  subspopn  29846  prdsbnd  29890  heibor1lem  29906  heiborlem1  29908  heibor  29918  isdrngo2  29962  rngoisocnv  29985  maxidlmax  30041  rexrabdioph  30329  ctbnfien  30354  irrapxlem3  30362  elpell14qr2  30400  elpell1qr2  30410  kelac1  30613  lcmgcdlem  30812  nznngen  30821  tz6.12-afv  31725  ellcoellss  32109  lindslinindsimp2  32137  riotasv3d  33763  lkrpssN  33960  intnatN  34203  elpaddatiN  34601  pexmidlem5N  34770  lhpj1  34818  ltrnu  34917  cdlemn11pre  36007  dihord2pre  36022  dih1dimatlem0  36125  lcfrlem9  36347
  Copyright terms: Public domain W3C validator