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

Theorem impr 603
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 423 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  moi2  3075  preq12bg  3937  disjxiun  4169  disjxun  4170  wereu2  4539  frsn  4907  suppssr  5823  f1ocnv2d  6254  riotasv3d  6557  omeulem1  6784  oelim2  6797  oeoa  6799  boxriin  7063  frfi  7311  fipreima  7370  marypha1lem  7396  supiso  7433  ordtypelem10  7452  cantnfreslem  7587  r1ordg  7660  infxpenc2lem1  7856  acndom  7888  acndom2  7891  cofsmo  8105  cfcoflem  8108  fin23lem28  8176  fin23lem36  8184  isf32lem1  8189  isf32lem2  8190  isf32lem5  8193  isf34lem4  8213  fin1a2lem6  8241  fin1a2s  8250  ttukeylem2  8346  ttukeylem6  8350  fpwwe2lem8  8468  fpwwe2lem12  8472  inar1  8606  grudomon  8648  axpre-sup  9000  prodge0  9813  un0addcl  10209  un0mulcl  10210  peano2uz2  10313  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  xlemul1a  10823  elfz2nn0  11038  fzind2  11153  expaddz  11379  expmulz  11381  cau3lem  12113  lo1bdd2  12273  climuni  12301  fsumcom2  12513  dvdsval2  12810  algcvga  13025  iserodd  13164  prmpwdvds  13227  ram0  13345  catpropd  13890  isgrpinv  14810  gicsubgen  15020  sylow2alem2  15207  sylow2a  15208  frgpuptinv  15358  ablfac1eu  15586  dvdsrcl2  15710  islss4  15993  lspsnel6  16025  lmhmima  16078  lsmcl  16110  gsumbagdiag  16396  psrass1lem  16397  coe1tmmul2  16623  epttop  17028  neindisj  17136  neitr  17198  restcls  17199  restntr  17200  ordtrest2lem  17221  cncnp  17298  cnconst  17302  1stcrest  17469  2ndcdisj  17472  2ndcsep  17475  1stccnp  17478  islly2  17500  1stckgenlem  17538  ptbasin  17562  ptbasfi  17566  ptcnplem  17606  ptcnp  17607  tx1stc  17635  qtophmeo  17802  filcon  17868  filuni  17870  ufileu  17904  elfm3  17935  rnelfmlem  17937  fmfnfmlem4  17942  cnpflf2  17985  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem4  18039  ptcmplem5  18040  tsmsxplem1  18135  bl2in  18383  metcnpi  18527  metcnpi2  18528  metcnpi3  18529  recld2  18798  icoopnst  18917  iocopnst  18918  iscfil3  19179  iscmet3lem2  19198  ovoliunlem1  19351  ovolicc2lem2  19367  ovolicc2lem4  19369  voliun  19401  volsuplem  19402  dyadmbllem  19444  mbfinf  19510  mbflimsup  19511  itg2seq  19587  itg2splitlem  19593  itg2cnlem1  19606  ellimc3  19719  dvnadd  19768  dvcnvlem  19813  c1liplem1  19833  lhop2  19852  coe1mul3  19975  ply1divex  20012  dvdsq1p  20036  aannenlem1  20198  aalioulem2  20203  dvtaylp  20239  ulmdvlem3  20271  iblulm  20276  cxpmul2z  20535  leibpilem1  20733  xrlimcnp  20760  wilthlem2  20805  basellem3  20818  dvdsflsumcom  20926  perfect  20968  dchreq  20995  dchrsum  21006  bposlem1  21021  lgsquad2  21097  dchrisum0fno1  21158  pntibnd  21240  spthispth  21526  ghgrp  21909  ghablo  21910  nmcvcn  22144  ubthlem1  22325  leopmul2i  23591  hstel2  23675  atom1d  23809  cdj1i  23889  f1o3d  23994  esumcst  24408  lgambdd  24774  cvmscld  24913  fprodcom2  25261  nofulllem4  25573  ax5seglem5  25776  axeuclid  25806  cgrxfr  25893  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnclem3  26157  finminlem  26211  nn0prpwlem  26215  neibastop1  26278  neibastop2lem  26279  tailfb  26296  fzadd2  26335  subspopn  26348  prdsbnd  26392  heibor1lem  26408  heiborlem1  26410  heibor  26420  isdrngo2  26464  rngoisocnv  26487  maxidlmax  26543  rexrabdioph  26744  ctbnfien  26769  irrapxlem3  26777  elpell14qr2  26815  elpell1qr2  26825  kelac1  27029  dsmmlss  27078  gsumcom3fi  27323  tz6.12-afv  27904  swrdswrd  28011  swrdccatin12lem3c  28023  lkrpssN  29646  intnatN  29889  elpaddatiN  30287  pexmidlem5N  30456  lhpj1  30504  ltrnu  30603  cdlemn11pre  31693  dihord2pre  31708  dih1dimatlem0  31811  lcfrlem9  32033
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 178  df-an 361
  Copyright terms: Public domain W3C validator