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

Theorem impr 647
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 196  df-an 385
This theorem is referenced by:  reximddv2  3002  moi2  3354  preq12bg  4326  prel12g  4327  disjxiun  4579  disjxiunOLD  4580  disjxun  4581  wereu2  5035  f1ocnv2d  6784  extmptsuppeq  7206  suppssr  7213  omeulem1  7549  oelim2  7562  oeoa  7564  boxriin  7836  frfi  8090  fipreima  8155  marypha1lem  8222  supiso  8264  ordtypelem10  8315  r1ordg  8524  infxpenc2lem1  8725  acndom  8757  acndom2  8760  cofsmo  8974  cfcoflem  8977  fin23lem28  9045  fin23lem36  9053  isf32lem1  9058  isf32lem2  9059  isf32lem5  9062  isf34lem4  9082  fin1a2lem6  9110  fin1a2s  9119  ttukeylem2  9215  ttukeylem6  9219  fpwwe2lem8  9338  fpwwe2lem12  9342  inar1  9476  grudomon  9518  axpre-sup  9869  prodge0  10749  un0addcl  11203  un0mulcl  11204  peano2uz2  11341  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  xlemul1a  11990  fzadd2  12247  elfz2nn0  12300  fzind2  12448  expaddz  12766  expmulz  12768  swrdswrd  13312  swrdccatin12lem2c  13339  swrdccatin12  13342  cau3lem  13942  lo1bdd2  14103  climuni  14131  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  dvdsval2  14824  algcvga  15130  lcmgcdlem  15157  coprmproddvdslem  15214  divgcdcoprmex  15218  iserodd  15378  prmpwdvds  15446  ram0  15564  catpropd  16192  mrcmndind  17189  isgrpinv  17295  gicsubgen  17544  sylow2alem2  17856  sylow2a  17857  frgpuptinv  18007  ablfac1eu  18295  dvdsrcl2  18473  islss4  18783  lspsnel6  18815  lmhmima  18868  lsmcl  18904  gsumbagdiag  19197  psrass1lem  19198  coe1tmmul2  19467  psgnodpm  19753  dsmmlss  19907  islindf4  19996  gsumcom3fi  20025  dmatscmcl  20128  mdetdiaglem  20223  mdetunilem9  20245  pm2mp  20449  epttop  20623  neindisj  20731  neitr  20794  restcls  20795  restntr  20796  ordtrest2lem  20817  cncnp  20894  cnconst  20898  1stcrest  21066  2ndcdisj  21069  2ndcsep  21072  1stccnp  21075  islly2  21097  1stckgenlem  21166  ptbasin  21190  ptbasfi  21194  ptcnplem  21234  ptcnp  21235  tx1stc  21263  qtophmeo  21430  filcon  21497  filuni  21499  ufileu  21533  elfm3  21564  rnelfmlem  21566  fmfnfmlem4  21571  cnpflf2  21614  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem4  21669  ptcmplem5  21670  tsmsxplem1  21766  bl2in  22015  metcnpi  22159  metcnpi2  22160  metcnpi3  22161  recld2  22425  icoopnst  22546  iocopnst  22547  ncvs1  22765  iscfil3  22879  iscmet3lem2  22898  ovoliunlem1  23077  ovolicc2lem2  23093  ovolicc2lem4  23095  voliun  23129  volsuplem  23130  dyadmbllem  23173  mbfinf  23238  mbflimsup  23239  itg2seq  23315  itg2splitlem  23321  itg2cnlem1  23334  ellimc3  23449  dvnadd  23498  dvcnvlem  23543  c1liplem1  23563  lhop2  23582  coe1mul3  23663  ply1divex  23700  dvdsq1p  23724  aannenlem1  23887  aalioulem2  23892  dvtaylp  23928  ulmdvlem3  23960  iblulm  23965  cxpmul2z  24237  leibpilem1  24467  xrlimcnp  24495  lgambdd  24563  wilthlem2  24595  basellem3  24609  dvdsflsumcom  24714  perfect  24756  dchreq  24783  dchrsum  24794  bposlem1  24809  lgsquad2  24911  dchrisum0fno1  25000  pntibnd  25082  lmieu  25476  ax5seglem5  25613  axeuclid  25643  spthispth  26103  wwlkextsur  26259  wwlkext2clwwlk  26331  nmcvcn  26934  ubthlem1  27110  leopmul2i  28378  hstel2  28462  atom1d  28596  cdj1i  28676  f1o3d  28813  xrge0addge  28912  reff  29234  ordtrest2NEWlem  29296  esumcst  29452  eulerpartlemgh  29767  cvmscld  30509  nofulllem4  31104  cgrxfr  31332  finminlem  31482  nn0prpwlem  31487  neibastop1  31524  neibastop2lem  31525  tailfb  31542  finixpnum  32564  lindsenlbs  32574  matunitlindflem2  32576  poimirlem4  32583  poimirlem25  32604  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  heicant  32614  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnclem3  32633  ftc1anc  32663  subspopn  32718  prdsbnd  32762  heibor1lem  32778  heiborlem1  32780  heibor  32790  isdrngo2  32927  rngoisocnv  32950  maxidlmax  33012  riotasv3d  33264  lkrpssN  33468  intnatN  33711  elpaddatiN  34109  pexmidlem5N  34278  lhpj1  34326  ltrnu  34425  cdlemn11pre  35517  dihord2pre  35532  dih1dimatlem0  35635  lcfrlem9  35857  rexrabdioph  36376  ctbnfien  36400  irrapxlem3  36406  elpell14qr2  36444  elpell1qr2  36454  kelac1  36651  iunrelexpuztr  37030  rfovcnvfvd  37321  radcnvrat  37535  nznngen  37537  tz6.12-afv  39902  iccelpart  39971  lighneallem4  40065  perfectALTV  40166  bgoldbtbndlem3  40223  tgoldbach  40232  tgoldbachOLD  40239  pfxccatin12  40288  egrsubgr  40501  nbumgrvtx  40568  wwlksnextsur  41106  wwlksext2clwwlk  41231  fusgr2wsp2nb  41498  isassintop  41636  ellcoellss  42018  lindslinindsimp2  42046  aacllem  42356
  Copyright terms: Public domain W3C validator