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  3237  preq12bg  4149  prel12g  4150  disjxiun  4387  disjxun  4388  wereu2  4815  frsn  5007  suppssrOLD  5936  f1ocnv2d  6411  extmptsuppeq  6813  suppssr  6820  omeulem1  7121  oelim2  7134  oeoa  7136  boxriin  7405  frfi  7658  fipreima  7718  marypha1lem  7784  supiso  7823  ordtypelem10  7842  r1ordg  8086  infxpenc2lem1  8286  acndom  8322  acndom2  8325  cofsmo  8539  cfcoflem  8542  fin23lem28  8610  fin23lem36  8618  isf32lem1  8623  isf32lem2  8624  isf32lem5  8627  isf34lem4  8647  fin1a2lem6  8675  fin1a2s  8684  ttukeylem2  8780  ttukeylem6  8784  fpwwe2lem8  8905  fpwwe2lem12  8909  inar1  9043  grudomon  9085  axpre-sup  9437  prodge0  10277  un0addcl  10714  un0mulcl  10715  peano2uz2  10830  rpnnen1lem1  11080  rpnnen1lem2  11081  rpnnen1lem3  11082  rpnnen1lem5  11084  xlemul1a  11352  elfz2nn0  11581  fzind2  11738  expaddz  12009  expmulz  12011  swrdswrd  12456  swrdccatin12lem2c  12481  swrdccatin12  12484  cau3lem  12944  lo1bdd2  13104  climuni  13132  fsumcom2  13343  dvdsval2  13640  algcvga  13856  iserodd  14004  prmpwdvds  14067  ram0  14185  catpropd  14750  mrcmndind  15596  isgrpinv  15690  gicsubgen  15908  sylow2alem2  16221  sylow2a  16222  frgpuptinv  16372  ablfac1eu  16679  dvdsrcl2  16848  islss4  17149  lspsnel6  17181  lmhmima  17234  lsmcl  17270  gsumbagdiag  17552  psrass1lem  17553  coe1tmmul2  17837  psgnodpm  18127  dsmmlss  18278  islindf4  18376  gsumcom3fi  18409  mdetdiaglem  18520  mdetunilem9  18542  epttop  18729  neindisj  18837  neitr  18900  restcls  18901  restntr  18902  ordtrest2lem  18923  cncnp  19000  cnconst  19004  1stcrest  19173  2ndcdisj  19176  2ndcsep  19179  1stccnp  19182  islly2  19204  1stckgenlem  19242  ptbasin  19266  ptbasfi  19270  ptcnplem  19310  ptcnp  19311  tx1stc  19339  qtophmeo  19506  filcon  19572  filuni  19574  ufileu  19608  elfm3  19639  rnelfmlem  19641  fmfnfmlem4  19646  cnpflf2  19689  alexsubALTlem4  19738  ptcmplem3  19742  ptcmplem4  19743  ptcmplem5  19744  tsmsxplem1  19843  bl2in  20091  metcnpi  20235  metcnpi2  20236  metcnpi3  20237  recld2  20507  icoopnst  20627  iocopnst  20628  iscfil3  20900  iscmet3lem2  20919  ovoliunlem1  21101  ovolicc2lem2  21117  ovolicc2lem4  21119  voliun  21151  volsuplem  21152  dyadmbllem  21195  mbfinf  21259  mbflimsup  21260  itg2seq  21336  itg2splitlem  21342  itg2cnlem1  21355  ellimc3  21470  dvnadd  21519  dvcnvlem  21564  c1liplem1  21584  lhop2  21603  coe1mul3  21687  ply1divex  21724  dvdsq1p  21748  aannenlem1  21910  aalioulem2  21915  dvtaylp  21951  ulmdvlem3  21983  iblulm  21988  cxpmul2z  22252  leibpilem1  22451  xrlimcnp  22478  wilthlem2  22523  basellem3  22536  dvdsflsumcom  22644  perfect  22686  dchreq  22713  dchrsum  22724  bposlem1  22739  lgsquad2  22815  dchrisum0fno1  22876  pntibnd  22958  ax5seglem5  23314  axeuclid  23344  spthispth  23607  ghgrp  23990  ghablo  23991  nmcvcn  24225  ubthlem1  24406  leopmul2i  25674  hstel2  25758  atom1d  25892  cdj1i  25972  f1o3d  26082  ordtrest2NEWlem  26486  esumcst  26648  eulerpartlemgh  26895  lgambdd  27157  cvmscld  27296  fprodcom2  27629  nofulllem4  27980  cgrxfr  28220  finixpnum  28552  heicant  28564  mblfinlem3  28568  mblfinlem4  28569  itg2addnclem  28581  itg2addnclem3  28583  ftc1anc  28613  finminlem  28651  nn0prpwlem  28655  neibastop1  28718  neibastop2lem  28719  tailfb  28736  fzadd2  28775  subspopn  28786  prdsbnd  28830  heibor1lem  28846  heiborlem1  28848  heibor  28858  isdrngo2  28902  rngoisocnv  28925  maxidlmax  28981  rexrabdioph  29270  ctbnfien  29295  irrapxlem3  29303  elpell14qr2  29341  elpell1qr2  29351  kelac1  29554  tz6.12-afv  30217  wwlkextsur  30501  wwlkext2clwwlk  30603  ellcoellss  31076  lindslinindsimp2  31104  pmat2matp  31279  riotasv3d  32917  lkrpssN  33114  intnatN  33357  elpaddatiN  33755  pexmidlem5N  33924  lhpj1  33972  ltrnu  34071  cdlemn11pre  35161  dihord2pre  35176  dih1dimatlem0  35279  lcfrlem9  35501
  Copyright terms: Public domain W3C validator