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

Theorem expr 640
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
expr ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 628 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 443 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:  reximddv  3000  rexlimdvaa  3013  disjxiun  4573  disjxiunOLD  4574  wereu2  5025  ordtr3  5672  fcof1  6420  knatar  6485  riota5f  6513  ovmpt2df  6668  extmptsuppeq  7184  suppss  7190  suppss2  7194  wfrlem17  7296  smoord  7327  tfrlem9a  7347  oaass  7506  oelimcl  7545  oaabs2  7590  swoso  7640  eceqoveq  7718  domdifsn  7906  domunsncan  7923  omxpenlem  7924  enfixsn  7932  mapdom2  7994  frfi  8068  fofinf1o  8104  finsschain  8134  elfiun  8197  marypha1lem  8200  eqsupd  8224  eqinfd  8252  ordiso2  8281  ordtypelem6  8289  ordtypelem7  8290  ordtypelem10  8293  oismo  8306  wemapsolem  8316  brwdom2  8339  wdomtr  8341  unwdomg  8350  xpwdomg  8351  unxpwdom2  8354  cantnfval2  8427  cantnfle  8429  cantnflem1  8447  cantnf  8451  r1ordg  8502  tcrank  8608  carddomi2  8657  harval2  8684  infxpenlem  8697  infxpenc2lem2  8704  fseqenlem1  8708  dfac8clem  8716  acndom2  8738  infpwfien  8746  iunfictbso  8798  dfac12lem3  8828  infxp  8898  coflim  8944  cofsmo  8952  coftr  8956  sornom  8960  infpssrlem4  8989  enfin2i  9004  fin23lem26  9008  fin23lem27  9011  fin23lem36  9031  fin23lem40  9034  isf32lem5  9040  isf34lem4  9060  isfin1-3  9069  fin1a2lem10  9092  fin1a2lem13  9095  fin1a2s  9097  hsmexlem4  9112  ttukeylem5  9196  ttukeylem6  9197  ttukeylem7  9198  alephval2  9251  gchor  9306  fpwwe2lem7  9315  fpwwe2lem12  9320  fpwwe2  9322  pwfseqlem4a  9340  pwfseqlem4  9341  winalim2  9375  gchina  9378  inar1  9454  nqereq  9614  prlem934  9712  prlem936  9726  addsrmo  9751  mulsrmo  9752  supsrlem  9789  axpre-sup  9847  dedekind  10052  dedekindle  10053  prodge0  10722  mulge0b  10745  supaddc  10840  supmul1  10842  un0addcl  11176  un0mulcl  11177  uzwo3  11618  qbtwnre  11866  xlemul1a  11950  seqcl2  12639  seqfveq2  12643  seqshft2  12647  monoord  12651  seqsplit  12654  seqf1olem1  12660  seqid2  12667  seqhomo  12668  expnegz  12714  expcan  12733  ltexp2  12734  discr  12821  bcval5  12925  hashbc  13049  hashf1lem2  13052  seqcoll  13060  seqcoll2  13061  wrdind  13277  wrd2ind  13278  cau3lem  13891  ello1d  14051  lo1bdd2  14052  rlimclim  14074  climrlim2  14075  rlimdm  14079  rlimcn1  14116  reccn2  14124  rlimsqzlem  14176  lo1le  14179  caucvgrlem  14200  caurcvg2  14205  summolem2  14243  zsum  14245  fsum  14247  fsumf1o  14250  sumss  14251  fsumss  14252  fsumcl2lem  14258  fsumadd  14266  fsumcom2  14296  fsumcom2OLD  14297  fsum0diag2  14306  fsummulc2  14307  fsumconst  14313  fsumrelem  14329  fsumrlim  14333  fsumo1  14334  divrcnv  14372  geomulcvg  14395  mertenslem2  14405  prodmolem2  14453  zprod  14455  fprod  14459  fprodf1o  14464  prodss  14465  fprodss  14466  fprodcl2lem  14468  fprodmul  14478  fproddiv  14479  fprodconst  14496  fprodn0  14497  fprodcom2  14502  fprodcom2OLD  14503  ruclem8  14754  dvds0lem  14779  dvdsnegb  14786  dvdssub2  14810  bitsf1  14955  bitsshft  14984  bezoutlem3  15045  bezoutlem4  15046  isprm2lem  15181  isprm5  15206  isprm6  15213  hashgcdeq  15281  modprminv  15291  modprminveq  15292  reumodprminv  15296  pcqmul  15345  pcqcl  15348  pcxcl  15352  pc2dvds  15370  pcadd  15380  pcmpt  15383  pockthg  15397  infpnlem1  15401  prmreclem5  15411  vdwlem2  15473  vdwlem9  15480  vdwlem10  15481  vdwlem12  15483  ramub  15504  0ram  15511  ramub1lem2  15518  ramub1  15519  ramcl  15520  mreexexd  16080  mreexexdOLD  16081  acsfn2  16096  iscatd  16106  catpropd  16141  setcmon  16509  pleval2i  16736  psss  16986  mgmidsssn0  17041  mhmeql  17136  frmdss2  17172  frmdup3  17176  grprcan  17227  dfgrp3lem  17285  mulgnn0ass  17350  isnsg3  17400  ghmpreima  17454  ghmeql  17455  gaorber  17513  f1omvdco2  17640  psgnunilem1  17685  psgnunilem2  17687  oddvds  17738  gexdvds  17771  sylow1lem1  17785  odcau  17791  pgpssslw  17801  sylow2alem2  17805  sylow2blem3  17809  fislw  17812  lsmmod  17860  efgredlem  17932  frgpup3  17963  gsumval3  18080  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumconst  18106  gsumzmhm  18109  gsumzoppg  18116  gsum2d2lem  18144  ablfac1eulem  18243  pgpfac1lem5  18250  ablfaclem3  18258  issubdrg  18577  lss1d  18733  lmhmeql  18825  lspextmo  18826  lspsnat  18915  lsppratlem6  18922  islbs3  18925  lbsextlem4  18931  lidl1el  18988  mvrf1  19195  mplsubglem  19204  mpllsslem  19205  mplcoe1  19235  mplcoe5  19238  gsummoncoe1  19444  cnsubrg  19574  gsumfsum  19581  prmirredlem  19608  znidomb  19677  frgpcyg  19689  cssmre  19804  dsmmsubg  19854  dsmmlss  19855  frlmsslsp  19902  lindff1  19926  lindfrn  19927  mat1dimcrng  20050  mdetdiaglem  20171  mdetunilem7  20191  mdetunilem8  20192  mdetunilem9  20193  cpmatacl  20288  cpmatmcllem  20290  mp2pm2mplem4  20381  en2top  20548  toponmre  20655  topssnei  20686  innei  20687  clslp  20710  restcls  20743  restntr  20744  ordtrest2lem  20765  cnpco  20829  cncls2  20835  cncnpi  20840  cncnp  20842  cnconst2  20845  cnpdis  20855  lmcnp  20866  cnhaus  20916  isreg2  20939  cncmp  20953  tgcmp  20962  sscmp  20966  cmpfi  20969  cnconn  20983  iunconlem  20988  clscon  20991  1stcfb  21006  1stcrest  21014  2ndcctbss  21016  2ndcdisj  21017  1stcelcls  21022  1stccnp  21023  restnlly  21043  cldllycmp  21056  lly1stc  21057  dislly  21058  locfincmp  21087  comppfsc  21093  kgentopon  21099  kgenidm  21108  1stckgenlem  21114  kgencn3  21119  ptpjpre1  21132  ptbasin  21138  txcls  21165  tx2cn  21171  ptpjcn  21172  ptclsg  21176  ptcnp  21183  txdis  21193  txlly  21197  txnlly  21198  pthaus  21199  txtube  21201  txcmplem1  21202  txcmplem2  21203  txcmp  21204  txhaus  21208  txkgen  21213  xkohaus  21214  xkococnlem  21220  xkococn  21221  txcon  21250  qtopeu  21277  qtoprest  21278  regr1lem2  21301  kqreglem1  21302  cmphaushmeo  21361  xkocnv  21375  fgabs  21441  filuni  21447  trufil  21472  ufileu  21481  filufint  21482  fin1aufil  21494  elfm2  21510  rnelfmlem  21514  fmfnfmlem2  21517  fmfnfmlem4  21519  fmufil  21521  flimopn  21537  fbflim2  21539  hausflimi  21542  hausflim  21543  flimcf  21544  flimclslem  21546  flimsncls  21548  hauspwpwf1  21549  cnpflfi  21561  fclsnei  21581  fclscf  21587  flimfnfcls  21590  fclscmp  21592  ufilcmp  21594  fcfnei  21597  cnpfcf  21603  alexsublem  21606  alexsub  21607  alexsubALTlem2  21610  alexsubALTlem3  21611  alexsubALTlem4  21612  ptcmplem3  21616  ptcmplem4  21617  ptcmplem5  21618  symgtgp  21663  tgpconcompeqg  21673  tgpconcomp  21674  ghmcnp  21676  tgpt0  21680  qustgplem  21682  haustsms2  21698  tsmsgsum  21700  tsmsres  21705  tsmsxp  21716  imasdsf1olem  21936  xbln0  21977  blssps  21987  blss  21988  neibl  22064  blcld  22068  metss  22071  metequiv2  22073  met1stc  22084  metrest  22087  prdsxmslem2  22092  metcnp3  22103  nrmmetd  22137  nlmvscnlem1  22248  nrginvrcnlem  22253  nmoleub  22293  icccmplem2  22382  icccmp  22384  reconnlem2  22386  xrge0tsms  22393  metdstri  22410  metdseq0  22413  metdscn  22415  cnmpt2pc  22483  lebnumlem3  22518  pcoval2  22572  pcopt  22578  nmoleub2lem  22670  nmhmcn  22676  ipcnlem1  22797  cfilfcls  22825  cmetcaulem  22839  iscmet3lem2  22843  iscmet3  22844  equivcau  22851  caubl  22859  bcthlem2  22875  bcthlem3  22876  bcthlem4  22877  bcthlem5  22878  ivthlem2  22973  ivthlem3  22974  ovoliunlem2  23023  ovolicc2lem2  23038  ovolicc2lem3  23039  ovolicc2lem5  23041  ovolicc2  23042  ismbl2  23047  nulmbl  23055  nulmbl2  23056  unmbl  23057  shftmbl  23058  voliunlem3  23072  volsup  23076  ioombl1lem4  23081  ioombl1  23082  icombl  23084  ioombl  23085  uniioombl  23108  opnmbllem  23120  volivth  23126  vitali  23133  mbflimsup  23184  i1fadd  23213  itg1addlem4  23217  itg2le  23257  itg2seq  23260  itg2lea  23262  itg2splitlem  23266  itg2split  23267  itg2mono  23271  itg2gt0  23278  itg2cnlem2  23280  itgss  23329  itgfsum  23344  itgcn  23360  ellimc3  23394  limcco  23408  limciun  23409  dvnres  23445  dvnfre  23466  rolle  23502  c1liplem1  23508  dvivth  23522  dvne0  23523  lhop1lem  23525  lhop1  23526  lhop  23528  dvcnvrelem1  23529  dvfsumrlim  23543  dvfsum2  23546  ftc1a  23549  ftc1lem6  23553  itgsubst  23561  tdeglem4  23569  mdegaddle  23583  mdegvscale  23584  mdegmullem  23587  deg1tmle  23626  ply1divex  23645  dvdsq1p  23669  fta1g  23676  fta1b  23678  plyco0  23697  coeeulem  23729  dgrlem  23734  plyco  23746  coemullem  23755  dgreq0  23770  dgrco  23780  plydivex  23801  quotcan  23813  aannenlem1  23832  aalioulem2  23837  aalioulem3  23838  taylthlem1  23876  ulmbdd  23901  itgulm  23911  radcnvlt1  23921  psercnlem1  23928  abelthlem2  23935  abelthlem8  23942  logcnlem5  24137  efopn  24149  cxpmul2z  24182  cxpcn3lem  24233  cxpeq  24243  xrlimcnp  24440  cxplim  24443  o1cxp  24446  cxploglim  24449  scvxcvx  24457  jensen  24460  ftalem1  24544  ftalem2  24545  fta  24551  basellem3  24554  isppw2  24586  ppinprm  24623  chtnprm  24625  dvdsmulf1o  24665  chtublem  24681  perfectlem2  24700  dchrfi  24725  dchrptlem1  24734  dchrptlem2  24735  dchrptlem3  24736  dchrsum2  24738  bposlem1  24754  bposlem3  24756  2sqlem5  24892  2sqlem6  24893  2sqlem8  24896  2sqlem10  24898  2sqb  24902  chebbnd1lem1  24903  chtppilimlem2  24908  dchrisum0flb  24944  dchrisum0fno1  24945  dchrisum0  24954  pntrsumbnd2  25001  pntpbnd1  25020  pntpbnd2  25021  pntlemp  25044  pnt3  25046  qabvle  25059  ostth2lem2  25068  ostth3  25072  ostth  25073  colinearalglem4  25535  axcontlem10  25599  umgraex  25646  eupai  26288  numclwwlkovf2ex  26407  smcnlem  26765  ubthlem1  26944  ubthlem3  26946  htthlem  26992  5oalem6  27736  leopmuli  28210  pjnormssi  28245  pjclem4  28276  pj3si  28284  hatomistici  28439  sumdmdlem  28495  xrge0tsmsd  28950  isarchiofld  28982  ordtrest2NEWlem  29130  qqhf  29192  eulerpartlemb  29591  ballotlemfc0  29715  ballotlemfcc  29716  sgn3da  29764  subfacp1lem5  30254  erdszelem7  30267  erdszelem11  30271  pconcon  30301  txpcon  30302  conpcon  30305  sconpi1  30309  txscon  30311  cvxscon  30313  cvmopnlem  30348  cvmfolem  30349  cvmliftmolem2  30352  cvmliftlem7  30361  cvmliftlem10  30364  cvmlift2lem10  30382  cvmlift3lem4  30392  cvmlift3lem8  30396  msubff1  30541  wzel  30849  wzelOLD  30850  wsuclem  30851  wsuclemOLD  30852  nofulllem4  30938  btwnouttr2  31133  cgrxfr  31166  btwnxfr  31167  brcolinear  31170  lineext  31187  btwnconn1lem13  31210  midofsegid  31215  segcon2  31216  brsegle  31219  seglecgr12im  31221  segletr  31225  colinbtwnle  31229  broutsideof2  31233  btwnoutside  31236  broutsideof3  31237  outsideoftr  31240  outsideofeq  31241  outsideofeu  31242  outsidele  31243  lineunray  31258  lineelsb2  31259  linethru  31264  finminlem  31316  nn0prpwlem  31321  neibastop2lem  31359  neibastop2  31360  neibastop3  31361  topjoin  31364  tailfb  31376  relowlssretop  32211  wl-sbcom2d-lem1  32345  finixpnum  32388  poimirlem6  32409  poimirlem7  32410  poimirlem13  32416  poimirlem26  32429  poimirlem29  32432  heicant  32438  opnmbllem0  32439  mblfinlem3  32442  ismblfin  32444  ovoliunnfl  32445  voliunnfl  32447  volsupnfl  32448  itg2addnclem  32455  itg2addnclem3  32457  ftc1cnnc  32478  sdclem2  32532  fdc  32535  istotbnd3  32564  isbnd2  32576  isbnd3  32577  prdsbnd  32586  cntotbnd  32589  heibor1lem  32602  heibor1  32603  heiborlem10  32613  rrncmslem  32625  ghomco  32684  1idl  32819  unichnidl  32824  prtlem10  32992  prtlem18  33004  atlatmstc  33448  cvrexchlem  33547  paddasslem14  33961  pexmidlem5N  34102  cdleme29ex  34504  cdlemefr29exN  34532  cdleme32fva  34567  diarnN  35260  dihlsscpre  35365  isnacs3  36115  fnwe2lem2  36463  kelac1  36475  hbtlem5  36541  hbt  36543  dgraa0p  36562  rlimdmafv  39731  smonoord  39769  fmtnoprmfac2  39842  perfectALTVlem2  39990  upgrex  40340  av-numclwwlkovf2ex  41539  mgmhmeql  41615  lindslinindsimp2  42068
  Copyright terms: Public domain W3C validator