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

Theorem impr 456
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 414 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 420 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  reximddv2  3202  moi2  3656  preq12bg  4790  disjxiun  5078  disjxun  5079  wereu2  5597  frpomin  6258  f1ocnv2d  7554  funeldmdif  7921  extmptsuppeq  8035  suppssr  8043  suppssrg  8044  omeulem1  8444  oelim2  8457  oeoa  8459  boxriin  8759  frfi  9107  fipreima  9173  marypha1lem  9240  supiso  9282  ordtypelem10  9334  r1ordg  9584  infxpenc2lem1  9825  acndom  9857  acndom2  9860  cofsmo  10075  cfcoflem  10078  fin23lem28  10146  fin23lem36  10154  isf32lem1  10159  isf32lem2  10160  isf32lem5  10163  isf34lem4  10183  fin1a2lem6  10211  fin1a2s  10220  ttukeylem2  10316  ttukeylem6  10320  fpwwe2lem7  10443  fpwwe2lem11  10447  inar1  10581  grudomon  10623  axpre-sup  10975  un0addcl  12316  un0mulcl  12317  peano2uz2  12458  rpnnen1lem2  12767  rpnnen1lem1  12768  rpnnen1lem3  12769  rpnnen1lem5  12771  xlemul1a  13072  fzadd2  13341  elfz2nn0  13397  fzind2  13555  expaddz  13877  expmulz  13879  swrdswrd  14467  cau3lem  15115  lo1bdd2  15282  climuni  15310  fsumcom2  15535  fprodcom2  15743  dvdsval2  16015  algcvga  16333  lcmgcdlem  16360  coprmproddvdslem  16416  divgcdcoprmex  16420  iserodd  16585  prmpwdvds  16654  ram0  16772  catpropd  17467  mndind  18515  isgrpinv  18681  gicsubgen  18943  sylow2alem2  19272  sylow2a  19273  frgpuptinv  19426  gsumcom3fi  19629  gsumxp2  19630  ablfac1eu  19725  dvdsrcl2  19941  islss4  20273  lspsnel6  20305  lmhmima  20358  lsmcl  20394  psgnodpm  20842  dsmmlss  21000  islindf4  21094  gsumbagdiagOLD  21191  psrass1lemOLD  21192  gsumbagdiag  21194  psrass1lem  21195  coe1tmmul2  21496  dmatscmcl  21701  mdetdiaglem  21796  mdetunilem9  21818  pm2mp  22023  epttop  22208  neindisj  22317  neitr  22380  restcls  22381  restntr  22382  ordtrest2lem  22403  cncnp  22480  cnconst  22484  1stcrest  22653  2ndcdisj  22656  2ndcsep  22659  1stccnp  22662  islly2  22684  1stckgenlem  22753  ptbasin  22777  ptbasfi  22781  ptcnplem  22821  ptcnp  22822  tx1stc  22850  qtophmeo  23017  filconn  23083  filuni  23085  ufileu  23119  elfm3  23150  rnelfmlem  23152  fmfnfmlem4  23157  cnpflf2  23200  alexsubALTlem4  23250  ptcmplem3  23254  ptcmplem4  23255  ptcmplem5  23256  tsmsxplem1  23353  bl2in  23602  metcnpi  23749  metcnpi2  23750  metcnpi3  23751  recld2  24026  icoopnst  24151  iocopnst  24152  ncvs1  24370  iscfil3  24486  iscmet3lem2  24505  ovoliunlem1  24715  ovolicc2lem2  24731  ovolicc2lem4  24733  voliun  24767  volsuplem  24768  dyadmbllem  24812  mbfinf  24878  mbflimsup  24879  itg2seq  24956  itg2splitlem  24962  itg2cnlem1  24975  ellimc3  25092  dvnadd  25142  dvcnvlem  25189  c1liplem1  25209  lhop2  25228  coe1mul3  25313  ply1divex  25350  dvdsq1p  25374  aannenlem1  25537  aalioulem2  25542  dvtaylp  25578  ulmdvlem3  25610  iblulm  25615  cxpmul2z  25895  xrlimcnp  26167  lgambdd  26235  wilthlem2  26267  basellem3  26281  dvdsflsumcom  26386  perfect  26428  dchreq  26455  dchrsum  26466  bposlem1  26481  lgsquad2  26583  dchrisum0fno1  26708  pntibnd  26790  oppperpex  27163  lmieu  27194  ax5seglem5  27350  axeuclid  27380  egrsubgr  27693  nbumgrvtx  27762  wwlksnextsurj  28314  clwwlkccat  28403  numclwwlk2lem1lem  28755  nmcvcn  29106  ubthlem1  29281  leopmul2i  30546  hstel2  30630  atom1d  30764  cdj1i  30844  f1o3d  31011  fsuppcurry1  31109  fsuppcurry2  31110  xrge0addge  31129  prmidl0  31675  mxidlmax  31686  reff  31838  ordtrest2NEWlem  31921  esumcst  32080  eulerpartlemgh  32394  cvmscld  33284  noinfbnd1lem4  33978  madebdaylemlrcut  34128  cgrxfr  34406  finminlem  34556  nn0prpwlem  34560  neibastop1  34597  neibastop2lem  34598  tailfb  34615  fvineqsneu  35630  pibt2  35636  finixpnum  35810  lindsenlbs  35820  matunitlindflem2  35822  poimirlem4  35829  poimirlem25  35850  poimirlem26  35851  poimirlem29  35854  poimirlem30  35855  poimirlem31  35856  poimirlem32  35857  heicant  35860  mblfinlem3  35864  mblfinlem4  35865  itg2addnclem  35876  itg2addnclem3  35878  ftc1anc  35906  subspopn  35958  prdsbnd  35999  heibor1lem  36015  heiborlem1  36017  heibor  36027  isdrngo2  36164  rngoisocnv  36187  maxidlmax  36249  riotasv3d  37174  lkrpssN  37377  intnatN  37621  elpaddatiN  38019  pexmidlem5N  38188  lhpj1  38236  ltrnu  38335  cdlemn11pre  39424  dihord2pre  39439  dih1dimatlem0  39542  lcfrlem9  39764  remulcand  40615  prjspner1  40658  0prjspnrel  40659  prjcrv0  40665  nna4b4nsq  40692  rexrabdioph  40811  ctbnfien  40835  irrapxlem3  40841  elpell14qr2  40879  elpell1qr2  40889  kelac1  41084  iunrelexpuztr  41540  rfovcnvfvd  41828  radcnvrat  42145  nznngen  42147  tz6.12-afv  44909  tz6.12-afv2  44976  iccelpart  45129  prproropf1olem3  45201  lighneallem4  45306  perfectALTV  45419  bgoldbtbndlem3  45503  tgoldbach  45513  isomuspgr  45530  isassintop  45648  ellcoellss  46020  lindslinindsimp2  46048  itscnhlinecirc02plem3  46374  inlinecirc02p  46377  aacllem  46749
  Copyright terms: Public domain W3C validator