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

Theorem impr 455
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 413 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 419 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  reximddv2  3283  moi2  3711  preq12bg  4783  disjxiun  5060  disjxun  5061  wereu2  5551  f1ocnv2d  7388  funeldmdif  7738  extmptsuppeq  7845  suppssr  7852  omeulem1  8198  oelim2  8211  oeoa  8213  boxriin  8493  frfi  8752  fipreima  8819  marypha1lem  8886  supiso  8928  ordtypelem10  8980  r1ordg  9196  infxpenc2lem1  9434  acndom  9466  acndom2  9469  cofsmo  9680  cfcoflem  9683  fin23lem28  9751  fin23lem36  9759  isf32lem1  9764  isf32lem2  9765  isf32lem5  9768  isf34lem4  9788  fin1a2lem6  9816  fin1a2s  9825  ttukeylem2  9921  ttukeylem6  9925  fpwwe2lem8  10048  fpwwe2lem12  10052  inar1  10186  grudomon  10228  axpre-sup  10580  un0addcl  11919  un0mulcl  11920  peano2uz2  12059  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  xlemul1a  12671  fzadd2  12932  elfz2nn0  12988  fzind2  13145  expaddz  13463  expmulz  13465  swrdswrd  14057  cau3lem  14704  lo1bdd2  14871  climuni  14899  fsumcom2  15119  fprodcom2  15328  dvdsval2  15600  algcvga  15913  lcmgcdlem  15940  coprmproddvdslem  15996  divgcdcoprmex  16000  iserodd  16162  prmpwdvds  16230  ram0  16348  catpropd  16969  mndind  17975  isgrpinv  18086  gicsubgen  18348  sylow2alem2  18663  sylow2a  18664  frgpuptinv  18817  gsumcom3fi  19019  gsumxp2  19020  ablfac1eu  19115  dvdsrcl2  19320  islss4  19654  lspsnel6  19686  lmhmima  19739  lsmcl  19775  gsumbagdiag  20075  psrass1lem  20076  coe1tmmul2  20361  psgnodpm  20648  dsmmlss  20804  islindf4  20898  dmatscmcl  21028  mdetdiaglem  21123  mdetunilem9  21145  pm2mp  21349  epttop  21533  neindisj  21641  neitr  21704  restcls  21705  restntr  21706  ordtrest2lem  21727  cncnp  21804  cnconst  21808  1stcrest  21977  2ndcdisj  21980  2ndcsep  21983  1stccnp  21986  islly2  22008  1stckgenlem  22077  ptbasin  22101  ptbasfi  22105  ptcnplem  22145  ptcnp  22146  tx1stc  22174  qtophmeo  22341  filconn  22407  filuni  22409  ufileu  22443  elfm3  22474  rnelfmlem  22476  fmfnfmlem4  22481  cnpflf2  22524  alexsubALTlem4  22574  ptcmplem3  22578  ptcmplem4  22579  ptcmplem5  22580  tsmsxplem1  22676  bl2in  22925  metcnpi  23069  metcnpi2  23070  metcnpi3  23071  recld2  23337  icoopnst  23458  iocopnst  23459  ncvs1  23676  iscfil3  23791  iscmet3lem2  23810  ovoliunlem1  24018  ovolicc2lem2  24034  ovolicc2lem4  24036  voliun  24070  volsuplem  24071  dyadmbllem  24115  mbfinf  24181  mbflimsup  24182  itg2seq  24258  itg2splitlem  24264  itg2cnlem1  24277  ellimc3  24392  dvnadd  24441  dvcnvlem  24488  c1liplem1  24508  lhop2  24527  coe1mul3  24608  ply1divex  24645  dvdsq1p  24669  aannenlem1  24832  aalioulem2  24837  dvtaylp  24873  ulmdvlem3  24905  iblulm  24910  cxpmul2z  25187  leibpilem1OLD  25432  xrlimcnp  25460  lgambdd  25528  wilthlem2  25560  basellem3  25574  dvdsflsumcom  25679  perfect  25721  dchreq  25748  dchrsum  25759  bposlem1  25774  lgsquad2  25876  dchrisum0fno1  26001  pntibnd  26083  oppperpex  26453  lmieu  26484  ax5seglem5  26633  axeuclid  26663  egrsubgr  26973  nbumgrvtx  27042  wwlksnextsurj  27592  clwwlkccat  27682  numclwwlk2lem1lem  28035  nmcvcn  28386  ubthlem1  28561  leopmul2i  29826  hstel2  29910  atom1d  30044  cdj1i  30124  f1o3d  30287  fsuppcurry1  30374  fsuppcurry2  30375  xrge0addge  30394  reff  30989  ordtrest2NEWlem  31051  esumcst  31208  eulerpartlemgh  31522  cvmscld  32404  frpomin  32962  cgrxfr  33400  finminlem  33550  nn0prpwlem  33554  neibastop1  33591  neibastop2lem  33592  tailfb  33609  fvineqsneu  34561  pibt2  34567  finixpnum  34744  lindsenlbs  34754  matunitlindflem2  34756  poimirlem4  34763  poimirlem25  34784  poimirlem26  34785  poimirlem29  34788  poimirlem30  34789  poimirlem31  34790  poimirlem32  34791  heicant  34794  mblfinlem3  34798  mblfinlem4  34799  itg2addnclem  34810  itg2addnclem3  34812  ftc1anc  34842  subspopn  34895  prdsbnd  34939  heibor1lem  34955  heiborlem1  34957  heibor  34967  isdrngo2  35104  rngoisocnv  35127  maxidlmax  35189  riotasv3d  35963  lkrpssN  36166  intnatN  36410  elpaddatiN  36808  pexmidlem5N  36977  lhpj1  37025  ltrnu  37124  cdlemn11pre  38213  dihord2pre  38228  dih1dimatlem0  38331  lcfrlem9  38553  remulcand  39115  0prjspnrel  39134  rexrabdioph  39256  ctbnfien  39280  irrapxlem3  39286  elpell14qr2  39324  elpell1qr2  39334  kelac1  39528  iunrelexpuztr  39929  rfovcnvfvd  40218  radcnvrat  40511  nznngen  40513  tz6.12-afv  43238  tz6.12-afv2  43305  iccelpart  43425  prproropf1olem3  43499  lighneallem4  43607  perfectALTV  43720  bgoldbtbndlem3  43804  tgoldbach  43814  isomuspgr  43831  isassintop  43949  ellcoellss  44322  lindslinindsimp2  44350  itscnhlinecirc02plem3  44603  inlinecirc02p  44606  aacllem  44734
  Copyright terms: Public domain W3C validator