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

Theorem impr 602
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 422 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  moi2  2946  preq12bg  3791  disjxiun  4020  disjxun  4021  wereu2  4390  frsn  4760  suppssr  5659  f1ocnv2d  6068  riotasv3d  6353  omeulem1  6580  oelim2  6593  oeoa  6595  boxriin  6858  frfi  7102  fipreima  7161  marypha1lem  7186  supiso  7223  ordtypelem10  7242  cantnfreslem  7377  r1ordg  7450  infxpenc2lem1  7646  acndom  7678  acndom2  7681  cofsmo  7895  cfcoflem  7898  fin23lem28  7966  fin23lem36  7974  isf32lem1  7979  isf32lem2  7980  isf32lem5  7983  isf34lem4  8003  fin1a2lem6  8031  fin1a2s  8040  ttukeylem2  8137  ttukeylem6  8141  fpwwe2lem8  8259  fpwwe2lem12  8263  inar1  8397  grudomon  8439  axpre-sup  8791  prodge0  9603  un0addcl  9997  un0mulcl  9998  peano2uz2  10099  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  xlemul1a  10608  elfz2nn0  10821  fzind2  10923  expaddz  11146  expmulz  11148  cau3lem  11838  lo1bdd2  11998  climuni  12026  fsumcom2  12237  dvdsval2  12534  algcvga  12749  iserodd  12888  prmpwdvds  12951  ram0  13069  catpropd  13612  isgrpinv  14532  gicsubgen  14742  sylow2alem2  14929  sylow2a  14930  frgpuptinv  15080  ablfac1eu  15308  dvdsrcl2  15432  islss4  15719  lspsnel6  15751  lmhmima  15804  lsmcl  15836  gsumbagdiag  16122  psrass1lem  16123  coe1tmmul2  16352  epttop  16746  neindisj  16854  restcls  16911  restntr  16912  ordtrest2lem  16933  cncnp  17009  cnconst  17012  1stcrest  17179  2ndcdisj  17182  2ndcsep  17185  1stccnp  17188  islly2  17210  1stckgenlem  17248  ptbasin  17272  ptbasfi  17276  ptcnplem  17315  ptcnp  17316  tx1stc  17344  qtophmeo  17508  filcon  17578  filuni  17580  ufileu  17614  elfm3  17645  rnelfmlem  17647  fmfnfmlem4  17652  cnpflf2  17695  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem4  17749  ptcmplem5  17750  tsmsxplem1  17835  bl2in  17957  metcnpi  18090  metcnpi2  18091  metcnpi3  18092  recld2  18320  icoopnst  18437  iocopnst  18438  iscfil3  18699  iscmet3lem2  18718  ovoliunlem1  18861  ovolicc2lem2  18877  ovolicc2lem4  18879  voliun  18911  volsuplem  18912  dyadmbllem  18954  mbfinf  19020  mbflimsup  19021  itg2seq  19097  itg2splitlem  19103  itg2cnlem1  19116  ellimc3  19229  dvnadd  19278  dvcnvlem  19323  c1liplem1  19343  lhop2  19362  coe1mul3  19485  ply1divex  19522  dvdsq1p  19546  aannenlem1  19708  aalioulem2  19713  dvtaylp  19749  ulmdvlem3  19779  iblulm  19783  cxpmul2z  20038  leibpilem1  20236  xrlimcnp  20263  wilthlem2  20307  basellem3  20320  dvdsflsumcom  20428  perfect  20470  dchreq  20497  dchrsum  20508  bposlem1  20523  lgsquad2  20599  dchrisum0fno1  20660  pntibnd  20742  ghgrp  21035  ghablo  21036  nmcvcn  21268  ubthlem1  21449  leopmul2i  22715  hstel2  22799  atom1d  22933  cdj1i  23013  f1o3d  23037  cvmscld  23804  nofulllem4  24359  ax5seglem5  24561  axeuclid  24591  cgrxfr  24678  flfnei2  25577  islimrs3  25581  idmon  25817  cmp2morp  25958  finminlem  26231  nn0prpwlem  26238  neibastop1  26308  neibastop2lem  26309  tailfb  26326  fzadd2  26444  subspopn  26466  prdsbnd  26517  heibor1lem  26533  heiborlem1  26535  heibor  26545  isdrngo2  26589  rngoisocnv  26612  maxidlmax  26668  rexrabdioph  26875  ctbnfien  26901  irrapxlem3  26909  elpell14qr2  26947  elpell1qr2  26957  kelac1  27161  dsmmlss  27210  gsumcom3fi  27455  tz6.12-afv  28035  lkrpssN  29353  intnatN  29596  elpaddatiN  29994  pexmidlem5N  30163  lhpj1  30211  ltrnu  30310  cdlemn11pre  31400  dihord2pre  31415  dih1dimatlem0  31518  lcfrlem9  31740
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 177  df-an 360
  Copyright terms: Public domain W3C validator