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

Theorem impr 624
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 435 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  reximddv2  2903  moi2  3253  preq12bg  4177  prel12g  4178  disjxiun  4418  disjxun  4419  wereu2  4848  frsn  4922  f1ocnv2d  6532  extmptsuppeq  6948  suppssr  6955  omeulem1  7289  oelim2  7302  oeoa  7304  boxriin  7570  frfi  7820  fipreima  7884  marypha1lem  7951  supiso  7995  ordtypelem10  8046  r1ordg  8252  infxpenc2lem1  8452  acndom  8484  acndom2  8487  cofsmo  8701  cfcoflem  8704  fin23lem28  8772  fin23lem36  8780  isf32lem1  8785  isf32lem2  8786  isf32lem5  8789  isf34lem4  8809  fin1a2lem6  8837  fin1a2s  8846  ttukeylem2  8942  ttukeylem6  8946  fpwwe2lem8  9064  fpwwe2lem12  9068  inar1  9202  grudomon  9244  axpre-sup  9595  prodge0  10454  un0addcl  10905  un0mulcl  10906  peano2uz2  11025  rpnnen1lem1  11292  rpnnen1lem2  11293  rpnnen1lem3  11294  rpnnen1lem5  11296  xlemul1a  11576  elfz2nn0  11887  fzind2  12024  expaddz  12317  expmulz  12319  swrdswrd  12812  swrdccatin12lem2c  12840  swrdccatin12  12843  cau3lem  13411  lo1bdd2  13581  climuni  13609  fsumcom2  13828  fprodcom2  14031  dvdsval2  14301  algcvga  14531  lcmgcdlem  14564  coprmproddvdslem  14672  iserodd  14778  prmpwdvds  14841  ram0  14973  catpropd  15607  mrcmndind  16606  isgrpinv  16709  gicsubgen  16935  sylow2alem2  17263  sylow2a  17264  frgpuptinv  17414  ablfac1eu  17699  dvdsrcl2  17871  islss4  18178  lspsnel6  18210  lmhmima  18263  lsmcl  18299  gsumbagdiag  18593  psrass1lem  18594  coe1tmmul2  18862  psgnodpm  19148  dsmmlss  19299  islindf4  19388  gsumcom3fi  19417  dmatscmcl  19520  mdetdiaglem  19615  mdetunilem9  19637  pm2mp  19841  epttop  20016  neindisj  20125  neitr  20188  restcls  20189  restntr  20190  ordtrest2lem  20211  cncnp  20288  cnconst  20292  1stcrest  20460  2ndcdisj  20463  2ndcsep  20466  1stccnp  20469  islly2  20491  1stckgenlem  20560  ptbasin  20584  ptbasfi  20588  ptcnplem  20628  ptcnp  20629  tx1stc  20657  qtophmeo  20824  filcon  20890  filuni  20892  ufileu  20926  elfm3  20957  rnelfmlem  20959  fmfnfmlem4  20964  cnpflf2  21007  alexsubALTlem4  21057  ptcmplem3  21061  ptcmplem4  21062  ptcmplem5  21063  tsmsxplem1  21159  bl2in  21407  metcnpi  21551  metcnpi2  21552  metcnpi3  21553  recld2  21824  icoopnst  21959  iocopnst  21960  iscfil3  22235  iscmet3lem2  22254  ovoliunlem1  22447  ovolicc2lem2  22463  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  voliun  22499  volsuplem  22500  dyadmbllem  22549  mbfinf  22613  mbfinfOLD  22614  mbflimsup  22615  mbflimsupOLD  22616  itg2seq  22692  itg2splitlem  22698  itg2cnlem1  22711  ellimc3  22826  dvnadd  22875  dvcnvlem  22920  c1liplem1  22940  lhop2  22959  coe1mul3  23040  ply1divex  23079  dvdsq1p  23103  aannenlem1  23276  aalioulem2  23281  dvtaylp  23317  ulmdvlem3  23349  iblulm  23354  cxpmul2z  23628  leibpilem1  23858  xrlimcnp  23886  lgambdd  23954  wilthlem2  23986  basellem3  24001  dvdsflsumcom  24109  perfect  24151  dchreq  24178  dchrsum  24189  bposlem1  24204  lgsquad2  24280  dchrisum0fno1  24341  pntibnd  24423  lmieu  24818  ax5seglem5  24955  axeuclid  24985  spthispth  25295  wwlkextsur  25451  wwlkext2clwwlk  25523  ghgrpOLD  26088  ghabloOLD  26089  nmcvcn  26323  ubthlem1  26504  leopmul2i  27780  hstel2  27864  atom1d  27998  cdj1i  28078  f1o3d  28225  xrge0addge  28337  reff  28668  ordtrest2NEWlem  28730  esumcst  28886  eulerpartlemgh  29213  cvmscld  29998  nofulllem4  30593  cgrxfr  30821  finminlem  30973  nn0prpwlem  30977  neibastop1  31014  neibastop2lem  31015  tailfb  31032  finixpnum  31888  poimirlem4  31902  poimirlem25  31923  poimirlem26  31924  poimirlem29  31927  poimirlem30  31928  poimirlem31  31929  poimirlem32  31930  heicant  31933  mblfinlem3  31937  mblfinlem4  31938  itg2addnclem  31951  itg2addnclem3  31953  ftc1anc  31983  fzadd2  32028  subspopn  32039  prdsbnd  32083  heibor1lem  32099  heiborlem1  32101  heibor  32111  isdrngo2  32155  rngoisocnv  32178  maxidlmax  32234  riotasv3d  32495  lkrpssN  32692  intnatN  32935  elpaddatiN  33333  pexmidlem5N  33502  lhpj1  33550  ltrnu  33649  cdlemn11pre  34741  dihord2pre  34756  dih1dimatlem0  34859  lcfrlem9  35081  rexrabdioph  35600  ctbnfien  35624  irrapxlem3  35632  elpell14qr2  35672  elpell1qr2  35682  kelac1  35885  iunrelexpuztr  36215  radcnvrat  36565  nznngen  36567  tz6.12-afv  38431  iccelpart  38503  perfectALTV  38601  bgoldbtbndlem3  38658  tgoldbach  38667  pfxccatin12  38722  isassintop  39188  ellcoellss  39572  lindslinindsimp2  39600  aacllem  39884
  Copyright terms: Public domain W3C validator