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

Theorem impr 614
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:  moi2  3129  preq12bg  4039  prel12g  4040  disjxiun  4277  disjxun  4278  wereu2  4704  frsn  4896  suppssrOLD  5825  f1ocnv2d  6300  extmptsuppeq  6702  suppssr  6709  omeulem1  7009  oelim2  7022  oeoa  7024  boxriin  7293  frfi  7545  fipreima  7605  marypha1lem  7671  supiso  7710  ordtypelem10  7729  r1ordg  7973  infxpenc2lem1  8173  acndom  8209  acndom2  8212  cofsmo  8426  cfcoflem  8429  fin23lem28  8497  fin23lem36  8505  isf32lem1  8510  isf32lem2  8511  isf32lem5  8514  isf34lem4  8534  fin1a2lem6  8562  fin1a2s  8571  ttukeylem2  8667  ttukeylem6  8671  fpwwe2lem8  8792  fpwwe2lem12  8796  inar1  8930  grudomon  8972  axpre-sup  9324  prodge0  10164  un0addcl  10601  un0mulcl  10602  peano2uz2  10717  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem5  10971  xlemul1a  11239  elfz2nn0  11467  fzind2  11621  expaddz  11892  expmulz  11894  swrdswrd  12338  swrdccatin12lem2c  12363  swrdccatin12  12366  cau3lem  12826  lo1bdd2  12986  climuni  13014  fsumcom2  13225  dvdsval2  13521  algcvga  13737  iserodd  13885  prmpwdvds  13948  ram0  14066  catpropd  14631  mrcmndind  15476  isgrpinv  15568  gicsubgen  15786  sylow2alem2  16097  sylow2a  16098  frgpuptinv  16248  ablfac1eu  16548  dvdsrcl2  16676  islss4  16965  lspsnel6  16997  lmhmima  17050  lsmcl  17086  gsumbagdiag  17380  psrass1lem  17381  coe1tmmul2  17627  psgnodpm  17860  dsmmlss  18011  islindf4  18109  gsumcom3fi  18142  mdet1  18250  mdetunilem9  18268  epttop  18455  neindisj  18563  neitr  18626  restcls  18627  restntr  18628  ordtrest2lem  18649  cncnp  18726  cnconst  18730  1stcrest  18899  2ndcdisj  18902  2ndcsep  18905  1stccnp  18908  islly2  18930  1stckgenlem  18968  ptbasin  18992  ptbasfi  18996  ptcnplem  19036  ptcnp  19037  tx1stc  19065  qtophmeo  19232  filcon  19298  filuni  19300  ufileu  19334  elfm3  19365  rnelfmlem  19367  fmfnfmlem4  19372  cnpflf2  19415  alexsubALTlem4  19464  ptcmplem3  19468  ptcmplem4  19469  ptcmplem5  19470  tsmsxplem1  19569  bl2in  19817  metcnpi  19961  metcnpi2  19962  metcnpi3  19963  recld2  20233  icoopnst  20353  iocopnst  20354  iscfil3  20626  iscmet3lem2  20645  ovoliunlem1  20827  ovolicc2lem2  20843  ovolicc2lem4  20845  voliun  20877  volsuplem  20878  dyadmbllem  20921  mbfinf  20985  mbflimsup  20986  itg2seq  21062  itg2splitlem  21068  itg2cnlem1  21081  ellimc3  21196  dvnadd  21245  dvcnvlem  21290  c1liplem1  21310  lhop2  21329  coe1mul3  21456  ply1divex  21493  dvdsq1p  21517  aannenlem1  21679  aalioulem2  21684  dvtaylp  21720  ulmdvlem3  21752  iblulm  21757  cxpmul2z  22021  leibpilem1  22220  xrlimcnp  22247  wilthlem2  22292  basellem3  22305  dvdsflsumcom  22413  perfect  22455  dchreq  22482  dchrsum  22493  bposlem1  22508  lgsquad2  22584  dchrisum0fno1  22645  pntibnd  22727  ax5seglem5  23002  axeuclid  23032  spthispth  23295  ghgrp  23678  ghablo  23679  nmcvcn  23913  ubthlem1  24094  leopmul2i  25362  hstel2  25446  atom1d  25580  cdj1i  25660  f1o3d  25772  ordtrest2NEWlem  26206  esumcst  26368  eulerpartlemgh  26609  lgambdd  26871  cvmscld  27010  fprodcom2  27342  nofulllem4  27693  cgrxfr  27933  finixpnum  28258  heicant  28270  mblfinlem3  28274  mblfinlem4  28275  itg2addnclem  28287  itg2addnclem3  28289  ftc1anc  28319  finminlem  28357  nn0prpwlem  28361  neibastop1  28424  neibastop2lem  28425  tailfb  28442  fzadd2  28481  subspopn  28492  prdsbnd  28536  heibor1lem  28552  heiborlem1  28554  heibor  28564  isdrngo2  28608  rngoisocnv  28631  maxidlmax  28687  rexrabdioph  28977  ctbnfien  29002  irrapxlem3  29010  elpell14qr2  29048  elpell1qr2  29058  kelac1  29261  tz6.12-afv  29925  wwlkextsur  30209  wwlkext2clwwlk  30311  ellcoellss  30678  lindslinindsimp2  30706  riotasv3d  32184  lkrpssN  32381  intnatN  32624  elpaddatiN  33022  pexmidlem5N  33191  lhpj1  33239  ltrnu  33338  cdlemn11pre  34428  dihord2pre  34443  dih1dimatlem0  34546  lcfrlem9  34768
  Copyright terms: Public domain W3C validator