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  2920  moi2  3266  preq12bg  4194  prel12g  4195  disjxiun  4434  disjxun  4435  wereu2  4866  frsn  5060  suppssrOLD  6006  f1ocnv2d  6511  extmptsuppeq  6926  suppssr  6933  omeulem1  7233  oelim2  7246  oeoa  7248  boxriin  7513  frfi  7767  fipreima  7828  marypha1lem  7895  supiso  7936  ordtypelem10  7955  r1ordg  8199  infxpenc2lem1  8399  acndom  8435  acndom2  8438  cofsmo  8652  cfcoflem  8655  fin23lem28  8723  fin23lem36  8731  isf32lem1  8736  isf32lem2  8737  isf32lem5  8740  isf34lem4  8760  fin1a2lem6  8788  fin1a2s  8797  ttukeylem2  8893  ttukeylem6  8897  fpwwe2lem8  9018  fpwwe2lem12  9022  inar1  9156  grudomon  9198  axpre-sup  9549  prodge0  10395  un0addcl  10835  un0mulcl  10836  peano2uz2  10956  rpnnen1lem1  11217  rpnnen1lem2  11218  rpnnen1lem3  11219  rpnnen1lem5  11221  xlemul1a  11489  elfz2nn0  11777  fzind2  11903  expaddz  12189  expmulz  12191  swrdswrd  12664  swrdccatin12lem2c  12692  swrdccatin12  12695  cau3lem  13166  lo1bdd2  13326  climuni  13354  fsumcom2  13568  dvdsval2  13866  algcvga  14085  iserodd  14236  prmpwdvds  14299  ram0  14417  catpropd  14981  mrcmndind  15871  isgrpinv  15974  gicsubgen  16200  sylow2alem2  16512  sylow2a  16513  frgpuptinv  16663  ablfac1eu  16998  dvdsrcl2  17173  islss4  17482  lspsnel6  17514  lmhmima  17567  lsmcl  17603  gsumbagdiag  17902  psrass1lem  17903  coe1tmmul2  18191  psgnodpm  18497  dsmmlss  18648  islindf4  18746  gsumcom3fi  18775  dmatscmcl  18878  mdetdiaglem  18973  mdetunilem9  18995  pm2mp  19199  epttop  19383  neindisj  19491  neitr  19554  restcls  19555  restntr  19556  ordtrest2lem  19577  cncnp  19654  cnconst  19658  1stcrest  19827  2ndcdisj  19830  2ndcsep  19833  1stccnp  19836  islly2  19858  1stckgenlem  19927  ptbasin  19951  ptbasfi  19955  ptcnplem  19995  ptcnp  19996  tx1stc  20024  qtophmeo  20191  filcon  20257  filuni  20259  ufileu  20293  elfm3  20324  rnelfmlem  20326  fmfnfmlem4  20331  cnpflf2  20374  alexsubALTlem4  20423  ptcmplem3  20427  ptcmplem4  20428  ptcmplem5  20429  tsmsxplem1  20528  bl2in  20776  metcnpi  20920  metcnpi2  20921  metcnpi3  20922  recld2  21192  icoopnst  21312  iocopnst  21313  iscfil3  21585  iscmet3lem2  21604  ovoliunlem1  21786  ovolicc2lem2  21802  ovolicc2lem4  21804  voliun  21837  volsuplem  21838  dyadmbllem  21881  mbfinf  21945  mbflimsup  21946  itg2seq  22022  itg2splitlem  22028  itg2cnlem1  22041  ellimc3  22156  dvnadd  22205  dvcnvlem  22250  c1liplem1  22270  lhop2  22289  coe1mul3  22373  ply1divex  22410  dvdsq1p  22434  aannenlem1  22596  aalioulem2  22601  dvtaylp  22637  ulmdvlem3  22669  iblulm  22674  cxpmul2z  22944  leibpilem1  23143  xrlimcnp  23170  wilthlem2  23215  basellem3  23228  dvdsflsumcom  23336  perfect  23378  dchreq  23405  dchrsum  23416  bposlem1  23431  lgsquad2  23507  dchrisum0fno1  23568  pntibnd  23650  lmieu  24022  ax5seglem5  24108  axeuclid  24138  spthispth  24447  wwlkextsur  24603  wwlkext2clwwlk  24675  ghgrpOLD  25242  ghabloOLD  25243  nmcvcn  25477  ubthlem1  25658  leopmul2i  26926  hstel2  27010  atom1d  27144  cdj1i  27224  f1o3d  27343  gsummpt2co  27644  reff  27715  ordtrest2NEWlem  27777  esumcst  27944  eulerpartlemgh  28190  lgambdd  28452  cvmscld  28591  fprodcom2  29089  nofulllem4  29440  cgrxfr  29680  finixpnum  30013  heicant  30024  mblfinlem3  30028  mblfinlem4  30029  itg2addnclem  30041  itg2addnclem3  30043  ftc1anc  30073  finminlem  30111  nn0prpwlem  30115  neibastop1  30152  neibastop2lem  30153  tailfb  30170  fzadd2  30209  subspopn  30220  prdsbnd  30264  heibor1lem  30280  heiborlem1  30282  heibor  30292  isdrngo2  30336  rngoisocnv  30359  maxidlmax  30415  rexrabdioph  30702  ctbnfien  30727  irrapxlem3  30735  elpell14qr2  30773  elpell1qr2  30783  kelac1  30984  radcnvrat  31171  lcmgcdlem  31188  nznngen  31197  tz6.12-afv  32096  isassintop  32371  ellcoellss  32771  lindslinindsimp2  32799  riotasv3d  34431  lkrpssN  34628  intnatN  34871  elpaddatiN  35269  pexmidlem5N  35438  lhpj1  35486  ltrnu  35585  cdlemn11pre  36677  dihord2pre  36692  dih1dimatlem0  36795  lcfrlem9  37017
  Copyright terms: Public domain W3C validator