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

Theorem impr 648
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 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 448 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  reximddv2  3049  moi2  3420  preq12bg  4417  prel12g  4418  disjxiun  4681  disjxiunOLD  4682  disjxun  4683  wereu2  5140  f1ocnv2d  6928  extmptsuppeq  7364  suppssr  7371  omeulem1  7707  oelim2  7720  oeoa  7722  boxriin  7992  frfi  8246  fipreima  8313  marypha1lem  8380  supiso  8422  ordtypelem10  8473  r1ordg  8679  infxpenc2lem1  8880  acndom  8912  acndom2  8915  cofsmo  9129  cfcoflem  9132  fin23lem28  9200  fin23lem36  9208  isf32lem1  9213  isf32lem2  9214  isf32lem5  9217  isf34lem4  9237  fin1a2lem6  9265  fin1a2s  9274  ttukeylem2  9370  ttukeylem6  9374  fpwwe2lem8  9497  fpwwe2lem12  9501  inar1  9635  grudomon  9677  axpre-sup  10028  prodge0  10908  un0addcl  11364  un0mulcl  11365  peano2uz2  11503  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  xlemul1a  12156  fzadd2  12414  elfz2nn0  12469  fzind2  12626  expaddz  12944  expmulz  12946  swrdswrd  13506  swrdccatin12lem2c  13534  swrdccatin12  13537  cau3lem  14138  lo1bdd2  14299  climuni  14327  fsumcom2  14549  fsumcom2OLD  14550  fprodcom2  14758  fprodcom2OLD  14759  dvdsval2  15030  algcvga  15339  lcmgcdlem  15366  coprmproddvdslem  15423  divgcdcoprmex  15427  iserodd  15587  prmpwdvds  15655  ram0  15773  catpropd  16416  mrcmndind  17413  isgrpinv  17519  gicsubgen  17767  sylow2alem2  18079  sylow2a  18080  frgpuptinv  18230  ablfac1eu  18518  dvdsrcl2  18696  islss4  19010  lspsnel6  19042  lmhmima  19095  lsmcl  19131  gsumbagdiag  19424  psrass1lem  19425  coe1tmmul2  19694  psgnodpm  19982  dsmmlss  20136  islindf4  20225  gsumcom3fi  20254  dmatscmcl  20357  mdetdiaglem  20452  mdetunilem9  20474  pm2mp  20678  epttop  20861  neindisj  20969  neitr  21032  restcls  21033  restntr  21034  ordtrest2lem  21055  cncnp  21132  cnconst  21136  1stcrest  21304  2ndcdisj  21307  2ndcsep  21310  1stccnp  21313  islly2  21335  1stckgenlem  21404  ptbasin  21428  ptbasfi  21432  ptcnplem  21472  ptcnp  21473  tx1stc  21501  qtophmeo  21668  filconn  21734  filuni  21736  ufileu  21770  elfm3  21801  rnelfmlem  21803  fmfnfmlem4  21808  cnpflf2  21851  alexsubALTlem4  21901  ptcmplem3  21905  ptcmplem4  21906  ptcmplem5  21907  tsmsxplem1  22003  bl2in  22252  metcnpi  22396  metcnpi2  22397  metcnpi3  22398  recld2  22664  icoopnst  22785  iocopnst  22786  ncvs1  23003  iscfil3  23117  iscmet3lem2  23136  ovoliunlem1  23316  ovolicc2lem2  23332  ovolicc2lem4  23334  voliun  23368  volsuplem  23369  dyadmbllem  23413  mbfinf  23477  mbflimsup  23478  itg2seq  23554  itg2splitlem  23560  itg2cnlem1  23573  ellimc3  23688  dvnadd  23737  dvcnvlem  23784  c1liplem1  23804  lhop2  23823  coe1mul3  23904  ply1divex  23941  dvdsq1p  23965  aannenlem1  24128  aalioulem2  24133  dvtaylp  24169  ulmdvlem3  24201  iblulm  24206  cxpmul2z  24482  leibpilem1  24712  xrlimcnp  24740  lgambdd  24808  wilthlem2  24840  basellem3  24854  dvdsflsumcom  24959  perfect  25001  dchreq  25028  dchrsum  25039  bposlem1  25054  lgsquad2  25156  dchrisum0fno1  25245  pntibnd  25327  lmieu  25721  ax5seglem5  25858  axeuclid  25888  egrsubgr  26214  nbumgrvtx  26287  wwlksnextsur  26863  wwlksext2clwwlkOLD  27022  numclwwlk2lem1lem  27324  nmcvcn  27678  ubthlem1  27854  leopmul2i  29122  hstel2  29206  atom1d  29340  cdj1i  29420  f1o3d  29559  xrge0addge  29650  reff  30034  ordtrest2NEWlem  30096  esumcst  30253  eulerpartlemgh  30568  cvmscld  31381  frpomin  31863  cgrxfr  32287  finminlem  32437  nn0prpwlem  32442  neibastop1  32479  neibastop2lem  32480  tailfb  32497  finixpnum  33524  lindsenlbs  33534  matunitlindflem2  33536  poimirlem4  33543  poimirlem25  33564  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  itg2addnclem3  33593  ftc1anc  33623  subspopn  33678  prdsbnd  33722  heibor1lem  33738  heiborlem1  33740  heibor  33750  isdrngo2  33887  rngoisocnv  33910  maxidlmax  33972  riotasv3d  34564  lkrpssN  34768  intnatN  35011  elpaddatiN  35409  pexmidlem5N  35578  lhpj1  35626  ltrnu  35725  cdlemn11pre  36816  dihord2pre  36831  dih1dimatlem0  36934  lcfrlem9  37156  rexrabdioph  37675  ctbnfien  37699  irrapxlem3  37705  elpell14qr2  37743  elpell1qr2  37753  kelac1  37950  iunrelexpuztr  38328  rfovcnvfvd  38618  radcnvrat  38830  nznngen  38832  tz6.12-afv  41574  iccelpart  41694  pfxccatin12  41750  lighneallem4  41852  perfectALTV  41957  bgoldbtbndlem3  42020  tgoldbach  42030  tgoldbachOLD  42037  isassintop  42171  ellcoellss  42549  lindslinindsimp2  42577  aacllem  42875
  Copyright terms: Public domain W3C validator