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  2959  preq12bg  3807  disjxiun  4036  disjxun  4037  wereu2  4406  frsn  4776  suppssr  5675  f1ocnv2d  6084  riotasv3d  6369  omeulem1  6596  oelim2  6609  oeoa  6611  boxriin  6874  frfi  7118  fipreima  7177  marypha1lem  7202  supiso  7239  ordtypelem10  7258  cantnfreslem  7393  r1ordg  7466  infxpenc2lem1  7662  acndom  7694  acndom2  7697  cofsmo  7911  cfcoflem  7914  fin23lem28  7982  fin23lem36  7990  isf32lem1  7995  isf32lem2  7996  isf32lem5  7999  isf34lem4  8019  fin1a2lem6  8047  fin1a2s  8056  ttukeylem2  8153  ttukeylem6  8157  fpwwe2lem8  8275  fpwwe2lem12  8279  inar1  8413  grudomon  8455  axpre-sup  8807  prodge0  9619  un0addcl  10013  un0mulcl  10014  peano2uz2  10115  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  xlemul1a  10624  elfz2nn0  10837  fzind2  10939  expaddz  11162  expmulz  11164  cau3lem  11854  lo1bdd2  12014  climuni  12042  fsumcom2  12253  dvdsval2  12550  algcvga  12765  iserodd  12904  prmpwdvds  12967  ram0  13085  catpropd  13628  isgrpinv  14548  gicsubgen  14758  sylow2alem2  14945  sylow2a  14946  frgpuptinv  15096  ablfac1eu  15324  dvdsrcl2  15448  islss4  15735  lspsnel6  15767  lmhmima  15820  lsmcl  15852  gsumbagdiag  16138  psrass1lem  16139  coe1tmmul2  16368  epttop  16762  neindisj  16870  restcls  16927  restntr  16928  ordtrest2lem  16949  cncnp  17025  cnconst  17028  1stcrest  17195  2ndcdisj  17198  2ndcsep  17201  1stccnp  17204  islly2  17226  1stckgenlem  17264  ptbasin  17288  ptbasfi  17292  ptcnplem  17331  ptcnp  17332  tx1stc  17360  qtophmeo  17524  filcon  17594  filuni  17596  ufileu  17630  elfm3  17661  rnelfmlem  17663  fmfnfmlem4  17668  cnpflf2  17711  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem4  17765  ptcmplem5  17766  tsmsxplem1  17851  bl2in  17973  metcnpi  18106  metcnpi2  18107  metcnpi3  18108  recld2  18336  icoopnst  18453  iocopnst  18454  iscfil3  18715  iscmet3lem2  18734  ovoliunlem1  18877  ovolicc2lem2  18893  ovolicc2lem4  18895  voliun  18927  volsuplem  18928  dyadmbllem  18970  mbfinf  19036  mbflimsup  19037  itg2seq  19113  itg2splitlem  19119  itg2cnlem1  19132  ellimc3  19245  dvnadd  19294  dvcnvlem  19339  c1liplem1  19359  lhop2  19378  coe1mul3  19501  ply1divex  19538  dvdsq1p  19562  aannenlem1  19724  aalioulem2  19729  dvtaylp  19765  ulmdvlem3  19795  iblulm  19799  cxpmul2z  20054  leibpilem1  20252  xrlimcnp  20279  wilthlem2  20323  basellem3  20336  dvdsflsumcom  20444  perfect  20486  dchreq  20513  dchrsum  20524  bposlem1  20539  lgsquad2  20615  dchrisum0fno1  20676  pntibnd  20758  ghgrp  21051  ghablo  21052  nmcvcn  21284  ubthlem1  21465  leopmul2i  22731  hstel2  22815  atom1d  22949  cdj1i  23029  f1o3d  23053  cvmscld  23819  nofulllem4  24430  ax5seglem5  24633  axeuclid  24663  cgrxfr  24750  itg2addnclem  25003  flfnei2  25680  islimrs3  25684  idmon  25920  cmp2morp  26061  finminlem  26334  nn0prpwlem  26341  neibastop1  26411  neibastop2lem  26412  tailfb  26429  fzadd2  26547  subspopn  26569  prdsbnd  26620  heibor1lem  26636  heiborlem1  26638  heibor  26648  isdrngo2  26692  rngoisocnv  26715  maxidlmax  26771  rexrabdioph  26978  ctbnfien  27004  irrapxlem3  27012  elpell14qr2  27050  elpell1qr2  27060  kelac1  27264  dsmmlss  27313  gsumcom3fi  27558  tz6.12-afv  28141  spthispth  28359  lkrpssN  29975  intnatN  30218  elpaddatiN  30616  pexmidlem5N  30785  lhpj1  30833  ltrnu  30932  cdlemn11pre  32022  dihord2pre  32037  dih1dimatlem0  32140  lcfrlem9  32362
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