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

Theorem impr 625
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  2866  moi2  3221  preq12bg  4157  prel12g  4158  disjxiun  4402  disjxun  4403  wereu2  4834  frsn  4908  f1ocnv2d  6525  extmptsuppeq  6944  suppssr  6951  omeulem1  7288  oelim2  7301  oeoa  7303  boxriin  7569  frfi  7821  fipreima  7885  marypha1lem  7952  supiso  7996  ordtypelem10  8047  r1ordg  8254  infxpenc2lem1  8455  acndom  8487  acndom2  8490  cofsmo  8704  cfcoflem  8707  fin23lem28  8775  fin23lem36  8783  isf32lem1  8788  isf32lem2  8789  isf32lem5  8792  isf34lem4  8812  fin1a2lem6  8840  fin1a2s  8849  ttukeylem2  8945  ttukeylem6  8949  fpwwe2lem8  9067  fpwwe2lem12  9071  inar1  9205  grudomon  9247  axpre-sup  9598  prodge0  10459  un0addcl  10910  un0mulcl  10911  peano2uz2  11030  rpnnen1lem1  11297  rpnnen1lem2  11298  rpnnen1lem3  11299  rpnnen1lem5  11301  xlemul1a  11581  elfz2nn0  11892  fzind2  12030  expaddz  12323  expmulz  12325  swrdswrd  12823  swrdccatin12lem2c  12851  swrdccatin12  12854  cau3lem  13429  lo1bdd2  13600  climuni  13628  fsumcom2  13847  fprodcom2  14050  dvdsval2  14320  algcvga  14550  lcmgcdlem  14583  coprmproddvdslem  14691  iserodd  14797  prmpwdvds  14860  ram0  14992  catpropd  15626  mrcmndind  16625  isgrpinv  16728  gicsubgen  16954  sylow2alem2  17282  sylow2a  17283  frgpuptinv  17433  ablfac1eu  17718  dvdsrcl2  17890  islss4  18197  lspsnel6  18229  lmhmima  18282  lsmcl  18318  gsumbagdiag  18612  psrass1lem  18613  coe1tmmul2  18881  psgnodpm  19168  dsmmlss  19319  islindf4  19408  gsumcom3fi  19437  dmatscmcl  19540  mdetdiaglem  19635  mdetunilem9  19657  pm2mp  19861  epttop  20036  neindisj  20145  neitr  20208  restcls  20209  restntr  20210  ordtrest2lem  20231  cncnp  20308  cnconst  20312  1stcrest  20480  2ndcdisj  20483  2ndcsep  20486  1stccnp  20489  islly2  20511  1stckgenlem  20580  ptbasin  20604  ptbasfi  20608  ptcnplem  20648  ptcnp  20649  tx1stc  20677  qtophmeo  20844  filcon  20910  filuni  20912  ufileu  20946  elfm3  20977  rnelfmlem  20979  fmfnfmlem4  20984  cnpflf2  21027  alexsubALTlem4  21077  ptcmplem3  21081  ptcmplem4  21082  ptcmplem5  21083  tsmsxplem1  21179  bl2in  21427  metcnpi  21571  metcnpi2  21572  metcnpi3  21573  recld2  21844  icoopnst  21979  iocopnst  21980  iscfil3  22255  iscmet3lem2  22274  ovoliunlem1  22467  ovolicc2lem2  22483  ovolicc2lem4OLD  22485  ovolicc2lem4  22486  voliun  22519  volsuplem  22520  dyadmbllem  22569  mbfinf  22633  mbfinfOLD  22634  mbflimsup  22635  mbflimsupOLD  22636  itg2seq  22712  itg2splitlem  22718  itg2cnlem1  22731  ellimc3  22846  dvnadd  22895  dvcnvlem  22940  c1liplem1  22960  lhop2  22979  coe1mul3  23060  ply1divex  23099  dvdsq1p  23123  aannenlem1  23296  aalioulem2  23301  dvtaylp  23337  ulmdvlem3  23369  iblulm  23374  cxpmul2z  23648  leibpilem1  23878  xrlimcnp  23906  lgambdd  23974  wilthlem2  24006  basellem3  24021  dvdsflsumcom  24129  perfect  24171  dchreq  24198  dchrsum  24209  bposlem1  24224  lgsquad2  24300  dchrisum0fno1  24361  pntibnd  24443  lmieu  24838  ax5seglem5  24975  axeuclid  25005  spthispth  25315  wwlkextsur  25471  wwlkext2clwwlk  25543  ghgrpOLD  26108  ghabloOLD  26109  nmcvcn  26343  ubthlem1  26524  leopmul2i  27800  hstel2  27884  atom1d  28018  cdj1i  28098  f1o3d  28241  xrge0addge  28349  reff  28678  ordtrest2NEWlem  28740  esumcst  28896  eulerpartlemgh  29223  cvmscld  30008  nofulllem4  30606  cgrxfr  30834  finminlem  30986  nn0prpwlem  30990  neibastop1  31027  neibastop2lem  31028  tailfb  31045  finixpnum  31942  poimirlem4  31956  poimirlem25  31977  poimirlem26  31978  poimirlem29  31981  poimirlem30  31982  poimirlem31  31983  poimirlem32  31984  heicant  31987  mblfinlem3  31991  mblfinlem4  31992  itg2addnclem  32005  itg2addnclem3  32007  ftc1anc  32037  fzadd2  32082  subspopn  32093  prdsbnd  32137  heibor1lem  32153  heiborlem1  32155  heibor  32165  isdrngo2  32209  rngoisocnv  32232  maxidlmax  32288  riotasv3d  32544  lkrpssN  32741  intnatN  32984  elpaddatiN  33382  pexmidlem5N  33551  lhpj1  33599  ltrnu  33698  cdlemn11pre  34790  dihord2pre  34805  dih1dimatlem0  34908  lcfrlem9  35130  rexrabdioph  35649  ctbnfien  35673  irrapxlem3  35680  elpell14qr2  35720  elpell1qr2  35730  kelac1  35933  iunrelexpuztr  36323  radcnvrat  36674  nznngen  36676  tz6.12-afv  38685  iccelpart  38757  perfectALTV  38855  bgoldbtbndlem3  38912  tgoldbach  38921  pfxccatin12  38976  egrsubgr  39359  nbumgrvtx  39424  isassintop  39950  ellcoellss  40332  lindslinindsimp2  40360  aacllem  40644
  Copyright terms: Public domain W3C validator