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

Theorem impr 617
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 432 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 431 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  reximddv2  2859  moi2  3205  preq12bg  4123  prel12g  4124  disjxiun  4364  disjxun  4365  wereu2  4790  frsn  4984  suppssrOLD  5923  f1ocnv2d  6425  extmptsuppeq  6842  suppssr  6849  omeulem1  7149  oelim2  7162  oeoa  7164  boxriin  7430  frfi  7680  fipreima  7741  marypha1lem  7808  supiso  7848  ordtypelem10  7867  r1ordg  8109  infxpenc2lem1  8309  acndom  8345  acndom2  8348  cofsmo  8562  cfcoflem  8565  fin23lem28  8633  fin23lem36  8641  isf32lem1  8646  isf32lem2  8647  isf32lem5  8650  isf34lem4  8670  fin1a2lem6  8698  fin1a2s  8707  ttukeylem2  8803  ttukeylem6  8807  fpwwe2lem8  8926  fpwwe2lem12  8930  inar1  9064  grudomon  9106  axpre-sup  9457  prodge0  10306  un0addcl  10746  un0mulcl  10747  peano2uz2  10867  rpnnen1lem1  11127  rpnnen1lem2  11128  rpnnen1lem3  11129  rpnnen1lem5  11131  xlemul1a  11401  elfz2nn0  11691  fzind2  11823  expaddz  12113  expmulz  12115  swrdswrd  12596  swrdccatin12lem2c  12624  swrdccatin12  12627  cau3lem  13189  lo1bdd2  13349  climuni  13377  fsumcom2  13591  fprodcom2  13790  dvdsval2  13991  algcvga  14210  iserodd  14361  prmpwdvds  14424  ram0  14542  catpropd  15115  mrcmndind  16114  isgrpinv  16217  gicsubgen  16443  sylow2alem2  16755  sylow2a  16756  frgpuptinv  16906  ablfac1eu  17237  dvdsrcl2  17412  islss4  17721  lspsnel6  17753  lmhmima  17806  lsmcl  17842  gsumbagdiag  18141  psrass1lem  18142  coe1tmmul2  18430  psgnodpm  18715  dsmmlss  18866  islindf4  18958  gsumcom3fi  18987  dmatscmcl  19090  mdetdiaglem  19185  mdetunilem9  19207  pm2mp  19411  epttop  19595  neindisj  19704  neitr  19767  restcls  19768  restntr  19769  ordtrest2lem  19790  cncnp  19867  cnconst  19871  1stcrest  20039  2ndcdisj  20042  2ndcsep  20045  1stccnp  20048  islly2  20070  1stckgenlem  20139  ptbasin  20163  ptbasfi  20167  ptcnplem  20207  ptcnp  20208  tx1stc  20236  qtophmeo  20403  filcon  20469  filuni  20471  ufileu  20505  elfm3  20536  rnelfmlem  20538  fmfnfmlem4  20543  cnpflf2  20586  alexsubALTlem4  20635  ptcmplem3  20639  ptcmplem4  20640  ptcmplem5  20641  tsmsxplem1  20740  bl2in  20988  metcnpi  21132  metcnpi2  21133  metcnpi3  21134  recld2  21404  icoopnst  21524  iocopnst  21525  iscfil3  21797  iscmet3lem2  21816  ovoliunlem1  21998  ovolicc2lem2  22014  ovolicc2lem4  22016  voliun  22049  volsuplem  22050  dyadmbllem  22093  mbfinf  22157  mbflimsup  22158  itg2seq  22234  itg2splitlem  22240  itg2cnlem1  22253  ellimc3  22368  dvnadd  22417  dvcnvlem  22462  c1liplem1  22482  lhop2  22501  coe1mul3  22585  ply1divex  22622  dvdsq1p  22646  aannenlem1  22809  aalioulem2  22814  dvtaylp  22850  ulmdvlem3  22882  iblulm  22887  cxpmul2z  23159  leibpilem1  23387  xrlimcnp  23415  wilthlem2  23460  basellem3  23473  dvdsflsumcom  23581  perfect  23623  dchreq  23650  dchrsum  23661  bposlem1  23676  lgsquad2  23752  dchrisum0fno1  23813  pntibnd  23895  lmieu  24270  ax5seglem5  24357  axeuclid  24387  spthispth  24696  wwlkextsur  24852  wwlkext2clwwlk  24924  ghgrpOLD  25487  ghabloOLD  25488  nmcvcn  25722  ubthlem1  25903  leopmul2i  27170  hstel2  27254  atom1d  27388  cdj1i  27468  f1o3d  27609  reff  27996  ordtrest2NEWlem  28058  esumcst  28211  eulerpartlemgh  28500  lgambdd  28768  cvmscld  28907  nofulllem4  29630  cgrxfr  29858  finixpnum  30203  heicant  30214  mblfinlem3  30218  mblfinlem4  30219  itg2addnclem  30232  itg2addnclem3  30234  ftc1anc  30264  finminlem  30302  nn0prpwlem  30306  neibastop1  30343  neibastop2lem  30344  tailfb  30361  fzadd2  30400  subspopn  30411  prdsbnd  30455  heibor1lem  30471  heiborlem1  30473  heibor  30483  isdrngo2  30527  rngoisocnv  30550  maxidlmax  30606  rexrabdioph  30893  ctbnfien  30917  irrapxlem3  30925  elpell14qr2  30963  elpell1qr2  30973  kelac1  31175  radcnvrat  31363  lcmgcdlem  31380  nznngen  31389  tz6.12-afv  32424  perfectALTV  32545  pfxccatin12  32600  isassintop  32852  ellcoellss  33236  lindslinindsimp2  33264  aacllem  33550  riotasv3d  35104  lkrpssN  35301  intnatN  35544  elpaddatiN  35942  pexmidlem5N  36111  lhpj1  36159  ltrnu  36258  cdlemn11pre  37350  dihord2pre  37365  dih1dimatlem0  37468  lcfrlem9  37690  iunrelexpuztr  38224
  Copyright terms: Public domain W3C validator