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:  moi2  3135  preq12bg  4046  prel12g  4047  disjxiun  4284  disjxun  4285  wereu2  4712  frsn  4904  suppssrOLD  5832  f1ocnv2d  6306  extmptsuppeq  6708  suppssr  6715  omeulem1  7013  oelim2  7026  oeoa  7028  boxriin  7297  frfi  7549  fipreima  7609  marypha1lem  7675  supiso  7714  ordtypelem10  7733  r1ordg  7977  infxpenc2lem1  8177  acndom  8213  acndom2  8216  cofsmo  8430  cfcoflem  8433  fin23lem28  8501  fin23lem36  8509  isf32lem1  8514  isf32lem2  8515  isf32lem5  8518  isf34lem4  8538  fin1a2lem6  8566  fin1a2s  8575  ttukeylem2  8671  ttukeylem6  8675  fpwwe2lem8  8796  fpwwe2lem12  8800  inar1  8934  grudomon  8976  axpre-sup  9328  prodge0  10168  un0addcl  10605  un0mulcl  10606  peano2uz2  10721  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  xlemul1a  11243  elfz2nn0  11472  fzind2  11629  expaddz  11900  expmulz  11902  swrdswrd  12346  swrdccatin12lem2c  12371  swrdccatin12  12374  cau3lem  12834  lo1bdd2  12994  climuni  13022  fsumcom2  13233  dvdsval2  13530  algcvga  13746  iserodd  13894  prmpwdvds  13957  ram0  14075  catpropd  14640  mrcmndind  15485  isgrpinv  15579  gicsubgen  15797  sylow2alem2  16108  sylow2a  16109  frgpuptinv  16259  ablfac1eu  16562  dvdsrcl2  16730  islss4  17020  lspsnel6  17052  lmhmima  17105  lsmcl  17141  gsumbagdiag  17423  psrass1lem  17424  coe1tmmul2  17704  psgnodpm  17993  dsmmlss  18144  islindf4  18242  gsumcom3fi  18275  mdet1  18383  mdetunilem9  18401  epttop  18588  neindisj  18696  neitr  18759  restcls  18760  restntr  18761  ordtrest2lem  18782  cncnp  18859  cnconst  18863  1stcrest  19032  2ndcdisj  19035  2ndcsep  19038  1stccnp  19041  islly2  19063  1stckgenlem  19101  ptbasin  19125  ptbasfi  19129  ptcnplem  19169  ptcnp  19170  tx1stc  19198  qtophmeo  19365  filcon  19431  filuni  19433  ufileu  19467  elfm3  19498  rnelfmlem  19500  fmfnfmlem4  19505  cnpflf2  19548  alexsubALTlem4  19597  ptcmplem3  19601  ptcmplem4  19602  ptcmplem5  19603  tsmsxplem1  19702  bl2in  19950  metcnpi  20094  metcnpi2  20095  metcnpi3  20096  recld2  20366  icoopnst  20486  iocopnst  20487  iscfil3  20759  iscmet3lem2  20778  ovoliunlem1  20960  ovolicc2lem2  20976  ovolicc2lem4  20978  voliun  21010  volsuplem  21011  dyadmbllem  21054  mbfinf  21118  mbflimsup  21119  itg2seq  21195  itg2splitlem  21201  itg2cnlem1  21214  ellimc3  21329  dvnadd  21378  dvcnvlem  21423  c1liplem1  21443  lhop2  21462  coe1mul3  21546  ply1divex  21583  dvdsq1p  21607  aannenlem1  21769  aalioulem2  21774  dvtaylp  21810  ulmdvlem3  21842  iblulm  21847  cxpmul2z  22111  leibpilem1  22310  xrlimcnp  22337  wilthlem2  22382  basellem3  22395  dvdsflsumcom  22503  perfect  22545  dchreq  22572  dchrsum  22583  bposlem1  22598  lgsquad2  22674  dchrisum0fno1  22735  pntibnd  22817  ax5seglem5  23130  axeuclid  23160  spthispth  23423  ghgrp  23806  ghablo  23807  nmcvcn  24041  ubthlem1  24222  leopmul2i  25490  hstel2  25574  atom1d  25708  cdj1i  25788  f1o3d  25899  ordtrest2NEWlem  26304  esumcst  26466  eulerpartlemgh  26713  lgambdd  26975  cvmscld  27114  fprodcom2  27446  nofulllem4  27797  cgrxfr  28037  finixpnum  28367  heicant  28379  mblfinlem3  28383  mblfinlem4  28384  itg2addnclem  28396  itg2addnclem3  28398  ftc1anc  28428  finminlem  28466  nn0prpwlem  28470  neibastop1  28533  neibastop2lem  28534  tailfb  28551  fzadd2  28590  subspopn  28601  prdsbnd  28645  heibor1lem  28661  heiborlem1  28663  heibor  28673  isdrngo2  28717  rngoisocnv  28740  maxidlmax  28796  rexrabdioph  29085  ctbnfien  29110  irrapxlem3  29118  elpell14qr2  29156  elpell1qr2  29166  kelac1  29369  tz6.12-afv  30032  wwlkextsur  30316  wwlkext2clwwlk  30418  mdetdiaglem  30824  ellcoellss  30858  lindslinindsimp2  30886  riotasv3d  32451  lkrpssN  32648  intnatN  32891  elpaddatiN  33289  pexmidlem5N  33458  lhpj1  33506  ltrnu  33605  cdlemn11pre  34695  dihord2pre  34710  dih1dimatlem0  34813  lcfrlem9  35035
  Copyright terms: Public domain W3C validator