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

Theorem impr 646
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
impr.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impr ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem impr
StepHypRef Expression
1 impr.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 448 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 447 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  reximddv2  3001  moi2  3353  preq12bg  4321  prel12g  4322  disjxiun  4573  disjxiunOLD  4574  disjxun  4575  wereu2  5024  f1ocnv2d  6761  extmptsuppeq  7183  suppssr  7190  omeulem1  7526  oelim2  7539  oeoa  7541  boxriin  7813  frfi  8067  fipreima  8132  marypha1lem  8199  supiso  8241  ordtypelem10  8292  r1ordg  8501  infxpenc2lem1  8702  acndom  8734  acndom2  8737  cofsmo  8951  cfcoflem  8954  fin23lem28  9022  fin23lem36  9030  isf32lem1  9035  isf32lem2  9036  isf32lem5  9039  isf34lem4  9059  fin1a2lem6  9087  fin1a2s  9096  ttukeylem2  9192  ttukeylem6  9196  fpwwe2lem8  9315  fpwwe2lem12  9319  inar1  9453  grudomon  9495  axpre-sup  9846  prodge0  10721  un0addcl  11175  un0mulcl  11176  peano2uz2  11299  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  xlemul1a  11949  fzadd2  12204  elfz2nn0  12257  fzind2  12405  expaddz  12723  expmulz  12725  swrdswrd  13260  swrdccatin12lem2c  13287  swrdccatin12  13290  cau3lem  13890  lo1bdd2  14051  climuni  14079  fsumcom2  14295  fsumcom2OLD  14296  fprodcom2  14501  fprodcom2OLD  14502  dvdsval2  14772  algcvga  15078  lcmgcdlem  15105  coprmproddvdslem  15162  divgcdcoprmex  15166  iserodd  15326  prmpwdvds  15394  ram0  15512  catpropd  16140  mrcmndind  17137  isgrpinv  17243  gicsubgen  17492  sylow2alem2  17804  sylow2a  17805  frgpuptinv  17955  ablfac1eu  18243  dvdsrcl2  18421  islss4  18731  lspsnel6  18763  lmhmima  18816  lsmcl  18852  gsumbagdiag  19145  psrass1lem  19146  coe1tmmul2  19415  psgnodpm  19700  dsmmlss  19854  islindf4  19943  gsumcom3fi  19972  dmatscmcl  20075  mdetdiaglem  20170  mdetunilem9  20192  pm2mp  20396  epttop  20570  neindisj  20678  neitr  20741  restcls  20742  restntr  20743  ordtrest2lem  20764  cncnp  20841  cnconst  20845  1stcrest  21013  2ndcdisj  21016  2ndcsep  21019  1stccnp  21022  islly2  21044  1stckgenlem  21113  ptbasin  21137  ptbasfi  21141  ptcnplem  21181  ptcnp  21182  tx1stc  21210  qtophmeo  21377  filcon  21444  filuni  21446  ufileu  21480  elfm3  21511  rnelfmlem  21513  fmfnfmlem4  21518  cnpflf2  21561  alexsubALTlem4  21611  ptcmplem3  21615  ptcmplem4  21616  ptcmplem5  21617  tsmsxplem1  21713  bl2in  21962  metcnpi  22106  metcnpi2  22107  metcnpi3  22108  recld2  22372  icoopnst  22493  iocopnst  22494  ncvs1  22709  iscfil3  22823  iscmet3lem2  22842  ovoliunlem1  23021  ovolicc2lem2  23037  ovolicc2lem4  23039  voliun  23073  volsuplem  23074  dyadmbllem  23117  mbfinf  23182  mbflimsup  23183  itg2seq  23259  itg2splitlem  23265  itg2cnlem1  23278  ellimc3  23393  dvnadd  23442  dvcnvlem  23487  c1liplem1  23507  lhop2  23526  coe1mul3  23607  ply1divex  23644  dvdsq1p  23668  aannenlem1  23831  aalioulem2  23836  dvtaylp  23872  ulmdvlem3  23904  iblulm  23909  cxpmul2z  24181  leibpilem1  24411  xrlimcnp  24439  lgambdd  24507  wilthlem2  24539  basellem3  24553  dvdsflsumcom  24658  perfect  24700  dchreq  24727  dchrsum  24738  bposlem1  24753  lgsquad2  24855  dchrisum0fno1  24944  pntibnd  25026  lmieu  25421  ax5seglem5  25558  axeuclid  25588  spthispth  25896  wwlkextsur  26052  wwlkext2clwwlk  26124  nmcvcn  26727  ubthlem1  26903  leopmul2i  28171  hstel2  28255  atom1d  28389  cdj1i  28469  f1o3d  28606  xrge0addge  28705  reff  29027  ordtrest2NEWlem  29089  esumcst  29245  eulerpartlemgh  29560  cvmscld  30302  nofulllem4  30897  cgrxfr  31125  finminlem  31275  nn0prpwlem  31280  neibastop1  31317  neibastop2lem  31318  tailfb  31335  finixpnum  32347  lindsenlbs  32357  matunitlindflem2  32359  poimirlem4  32366  poimirlem25  32387  poimirlem26  32388  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  poimirlem32  32394  heicant  32397  mblfinlem3  32401  mblfinlem4  32402  itg2addnclem  32414  itg2addnclem3  32416  ftc1anc  32446  subspopn  32501  prdsbnd  32545  heibor1lem  32561  heiborlem1  32563  heibor  32573  isdrngo2  32710  rngoisocnv  32733  maxidlmax  32795  riotasv3d  33047  lkrpssN  33251  intnatN  33494  elpaddatiN  33892  pexmidlem5N  34061  lhpj1  34109  ltrnu  34208  cdlemn11pre  35300  dihord2pre  35315  dih1dimatlem0  35418  lcfrlem9  35640  rexrabdioph  36159  ctbnfien  36183  irrapxlem3  36189  elpell14qr2  36227  elpell1qr2  36237  kelac1  36434  iunrelexpuztr  36813  rfovcnvfvd  37104  radcnvrat  37318  nznngen  37320  tz6.12-afv  39686  iccelpart  39755  lighneallem4  39849  perfectALTV  39950  bgoldbtbndlem3  40007  tgoldbach  40016  tgoldbachOLD  40023  pfxccatin12  40072  egrsubgr  40482  nbumgrvtx  40549  wwlksnextsur  41087  wwlksext2clwwlk  41212  fusgr2wsp2nb  41479  isassintop  41617  ellcoellss  41999  lindslinindsimp2  42027  aacllem  42298
  Copyright terms: Public domain W3C validator