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

Theorem impr 604
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 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 424 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  moi2  3116  preq12bg  3978  disjxiun  4210  disjxun  4211  wereu2  4580  frsn  4949  suppssr  5865  f1ocnv2d  6296  riotasv3d  6599  omeulem1  6826  oelim2  6839  oeoa  6841  boxriin  7105  frfi  7353  fipreima  7413  marypha1lem  7439  supiso  7478  ordtypelem10  7497  cantnfreslem  7632  r1ordg  7705  infxpenc2lem1  7901  acndom  7933  acndom2  7936  cofsmo  8150  cfcoflem  8153  fin23lem28  8221  fin23lem36  8229  isf32lem1  8234  isf32lem2  8235  isf32lem5  8238  isf34lem4  8258  fin1a2lem6  8286  fin1a2s  8295  ttukeylem2  8391  ttukeylem6  8395  fpwwe2lem8  8513  fpwwe2lem12  8517  inar1  8651  grudomon  8693  axpre-sup  9045  prodge0  9858  un0addcl  10254  un0mulcl  10255  peano2uz2  10358  rpnnen1lem1  10601  rpnnen1lem2  10602  rpnnen1lem3  10603  rpnnen1lem5  10605  xlemul1a  10868  elfz2nn0  11083  fzind2  11199  expaddz  11425  expmulz  11427  cau3lem  12159  lo1bdd2  12319  climuni  12347  fsumcom2  12559  dvdsval2  12856  algcvga  13071  iserodd  13210  prmpwdvds  13273  ram0  13391  catpropd  13936  isgrpinv  14856  gicsubgen  15066  sylow2alem2  15253  sylow2a  15254  frgpuptinv  15404  ablfac1eu  15632  dvdsrcl2  15756  islss4  16039  lspsnel6  16071  lmhmima  16124  lsmcl  16156  gsumbagdiag  16442  psrass1lem  16443  coe1tmmul2  16669  epttop  17074  neindisj  17182  neitr  17245  restcls  17246  restntr  17247  ordtrest2lem  17268  cncnp  17345  cnconst  17349  1stcrest  17517  2ndcdisj  17520  2ndcsep  17523  1stccnp  17526  islly2  17548  1stckgenlem  17586  ptbasin  17610  ptbasfi  17614  ptcnplem  17654  ptcnp  17655  tx1stc  17683  qtophmeo  17850  filcon  17916  filuni  17918  ufileu  17952  elfm3  17983  rnelfmlem  17985  fmfnfmlem4  17990  cnpflf2  18033  alexsubALTlem4  18082  ptcmplem3  18086  ptcmplem4  18087  ptcmplem5  18088  tsmsxplem1  18183  bl2in  18431  metcnpi  18575  metcnpi2  18576  metcnpi3  18577  recld2  18846  icoopnst  18965  iocopnst  18966  iscfil3  19227  iscmet3lem2  19246  ovoliunlem1  19399  ovolicc2lem2  19415  ovolicc2lem4  19417  voliun  19449  volsuplem  19450  dyadmbllem  19492  mbfinf  19558  mbflimsup  19559  itg2seq  19635  itg2splitlem  19641  itg2cnlem1  19654  ellimc3  19767  dvnadd  19816  dvcnvlem  19861  c1liplem1  19881  lhop2  19900  coe1mul3  20023  ply1divex  20060  dvdsq1p  20084  aannenlem1  20246  aalioulem2  20251  dvtaylp  20287  ulmdvlem3  20319  iblulm  20324  cxpmul2z  20583  leibpilem1  20781  xrlimcnp  20808  wilthlem2  20853  basellem3  20866  dvdsflsumcom  20974  perfect  21016  dchreq  21043  dchrsum  21054  bposlem1  21069  lgsquad2  21145  dchrisum0fno1  21206  pntibnd  21288  spthispth  21574  ghgrp  21957  ghablo  21958  nmcvcn  22192  ubthlem1  22373  leopmul2i  23639  hstel2  23723  atom1d  23857  cdj1i  23937  f1o3d  24042  esumcst  24456  lgambdd  24822  cvmscld  24961  fprodcom2  25309  nofulllem4  25661  ax5seglem5  25873  axeuclid  25903  cgrxfr  25990  mblfinlem3  26246  mblfinlem4  26247  itg2addnclem  26257  itg2addnclem3  26259  ftc1anc  26289  finminlem  26322  nn0prpwlem  26326  neibastop1  26389  neibastop2lem  26390  tailfb  26407  fzadd2  26446  subspopn  26459  prdsbnd  26503  heibor1lem  26519  heiborlem1  26521  heibor  26531  isdrngo2  26575  rngoisocnv  26598  maxidlmax  26654  rexrabdioph  26855  ctbnfien  26880  irrapxlem3  26888  elpell14qr2  26926  elpell1qr2  26936  kelac1  27139  dsmmlss  27188  gsumcom3fi  27433  tz6.12-afv  28014  swrdswrd  28200  swrdccatin12lem3c  28212  swrdccatin12  28215  lkrpssN  29962  intnatN  30205  elpaddatiN  30603  pexmidlem5N  30772  lhpj1  30820  ltrnu  30919  cdlemn11pre  32009  dihord2pre  32024  dih1dimatlem0  32127  lcfrlem9  32349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator