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

Theorem expr 642
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 630 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 444 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:  reximddv  3047  rexlimdvaa  3061  disjxiun  4681  disjxiunOLD  4682  wereu2  5140  ordtr3  5807  fcof1  6582  knatar  6647  riota5f  6676  ovmpt2df  6834  extmptsuppeq  7364  suppss  7370  suppss2  7374  wfrlem17  7476  smoord  7507  tfrlem9a  7527  oaass  7686  oelimcl  7725  oaabs2  7770  swoso  7820  eceqoveq  7895  domdifsn  8084  domunsncan  8101  omxpenlem  8102  enfixsn  8110  mapdom2  8172  frfi  8246  fofinf1o  8282  finsschain  8314  elfiun  8377  marypha1lem  8380  eqsupd  8404  eqinfd  8432  ordiso2  8461  ordtypelem6  8469  ordtypelem7  8470  ordtypelem10  8473  oismo  8486  wemapsolem  8496  brwdom2  8519  wdomtr  8521  unwdomg  8530  xpwdomg  8531  unxpwdom2  8534  cantnfval2  8604  cantnfle  8606  cantnflem1  8624  cantnf  8628  r1ordg  8679  tcrank  8785  carddomi2  8834  harval2  8861  infxpenlem  8874  infxpenc2lem2  8881  fseqenlem1  8885  dfac8clem  8893  acndom2  8915  infpwfien  8923  iunfictbso  8975  dfac12lem3  9005  infxp  9075  coflim  9121  cofsmo  9129  coftr  9133  sornom  9137  infpssrlem4  9166  enfin2i  9181  fin23lem26  9185  fin23lem27  9188  fin23lem36  9208  fin23lem40  9211  isf32lem5  9217  isf34lem4  9237  isfin1-3  9246  fin1a2lem10  9269  fin1a2lem13  9272  fin1a2s  9274  hsmexlem4  9289  ttukeylem5  9373  ttukeylem6  9374  ttukeylem7  9375  alephval2  9432  gchor  9487  fpwwe2lem7  9496  fpwwe2lem12  9501  fpwwe2  9503  pwfseqlem4a  9521  pwfseqlem4  9522  winalim2  9556  gchina  9559  inar1  9635  nqereq  9795  prlem934  9893  prlem936  9907  addsrmo  9932  mulsrmo  9933  supsrlem  9970  axpre-sup  10028  dedekind  10238  dedekindle  10239  prodge0  10908  mulge0b  10931  supaddc  11028  supmul1  11030  un0addcl  11364  un0mulcl  11365  uzwo3  11821  qbtwnre  12068  xlemul1a  12156  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqf1olem1  12880  seqid2  12887  seqhomo  12888  expnegz  12934  expcan  12953  ltexp2  12954  discr  13041  bcval5  13145  hashbc  13275  hashf1lem2  13278  seqcoll  13286  seqcoll2  13287  wrdind  13522  wrd2ind  13523  cau3lem  14138  ello1d  14298  lo1bdd2  14299  rlimclim  14321  climrlim2  14322  rlimdm  14326  rlimcn1  14363  reccn2  14371  rlimsqzlem  14423  lo1le  14426  caucvgrlem  14447  caurcvg2  14452  summolem2  14491  zsum  14493  fsum  14495  fsumf1o  14498  sumss  14499  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  fsumcom2  14549  fsumcom2OLD  14550  fsum0diag2  14559  fsummulc2  14560  fsumconst  14566  fsumrelem  14583  fsumrlim  14587  fsumo1  14588  divrcnv  14628  geomulcvg  14651  mertenslem2  14661  prodmolem2  14709  zprod  14711  fprod  14715  fprodf1o  14720  prodss  14721  fprodss  14722  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodconst  14752  fprodn0  14753  fprodcom2  14758  fprodcom2OLD  14759  ruclem8  15010  dvds0lem  15039  dvdsnegb  15046  dvdssub2  15070  bitsf1  15215  bitsshft  15244  bezoutlem3  15305  bezoutlem4  15306  isprm5  15466  isprm6  15473  hashgcdeq  15541  modprminv  15551  modprminveq  15552  reumodprminv  15556  pcqmul  15605  pcqcl  15608  pcxcl  15612  pc2dvds  15630  pcadd  15640  pcmpt  15643  pockthg  15657  infpnlem1  15661  prmreclem5  15671  vdwlem2  15733  vdwlem9  15740  vdwlem10  15741  vdwlem12  15743  ramub  15764  0ram  15771  ramub1lem2  15778  ramub1  15779  ramcl  15780  mreexexd  16355  mreexexdOLD  16356  acsfn2  16371  iscatd  16381  catpropd  16416  setcmon  16784  pleval2i  17011  psss  17261  mgmidsssn0  17316  mhmeql  17411  frmdss2  17447  frmdup3  17451  grprcan  17502  dfgrp3lem  17560  mulgnn0ass  17625  isnsg3  17675  ghmpreima  17729  ghmeql  17730  gaorber  17787  f1omvdco2  17914  psgnunilem1  17959  psgnunilem2  17961  oddvds  18012  gexdvds  18045  sylow1lem1  18059  odcau  18065  pgpssslw  18075  sylow2alem2  18079  sylow2blem3  18083  fislw  18086  lsmmod  18134  efgredlem  18206  frgpup3  18237  gsumval3  18354  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  gsum2d2lem  18418  ablfac1eulem  18517  pgpfac1lem5  18524  ablfaclem3  18532  issubdrg  18853  lss1d  19011  lmhmeql  19103  lspextmo  19104  lspsnat  19193  lsppratlem6  19200  islbs3  19203  lbsextlem4  19209  lidl1el  19266  mvrf1  19473  mplsubglem  19482  mpllsslem  19483  mplcoe1  19513  mplcoe5  19516  gsummoncoe1  19722  cnsubrg  19854  gsumfsum  19861  prmirredlem  19889  znidomb  19958  frgpcyg  19970  cssmre  20085  dsmmsubg  20135  dsmmlss  20136  frlmsslsp  20183  lindff1  20207  lindfrn  20208  mat1dimcrng  20331  mdetdiaglem  20452  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  cpmatacl  20569  cpmatmcllem  20571  mp2pm2mplem4  20662  en2top  20837  toponmre  20945  topssnei  20976  innei  20977  clslp  21000  restcls  21033  restntr  21034  ordtrest2lem  21055  cnpco  21119  cncls2  21125  cncnpi  21130  cncnp  21132  cnconst2  21135  cnpdis  21145  lmcnp  21156  cnhaus  21206  isreg2  21229  cncmp  21243  tgcmp  21252  sscmp  21256  cmpfi  21259  cnconn  21273  iunconnlem  21278  clsconn  21281  1stcfb  21296  1stcrest  21304  2ndcctbss  21306  2ndcdisj  21307  1stcelcls  21312  1stccnp  21313  restnlly  21333  cldllycmp  21346  lly1stc  21347  dislly  21348  locfincmp  21377  comppfsc  21383  kgentopon  21389  kgenidm  21398  1stckgenlem  21404  kgencn3  21409  ptpjpre1  21422  ptbasin  21428  txcls  21455  tx2cn  21461  ptpjcn  21462  ptclsg  21466  ptcnp  21473  txdis  21483  txlly  21487  txnlly  21488  pthaus  21489  txtube  21491  txcmplem1  21492  txcmplem2  21493  txcmp  21494  txhaus  21498  txkgen  21503  xkohaus  21504  xkococnlem  21510  xkococn  21511  txconn  21540  qtopeu  21567  qtoprest  21568  regr1lem2  21591  kqreglem1  21592  cmphaushmeo  21651  xkocnv  21665  fgabs  21730  filuni  21736  trufil  21761  ufileu  21770  filufint  21771  fin1aufil  21783  elfm2  21799  rnelfmlem  21803  fmfnfmlem2  21806  fmfnfmlem4  21808  fmufil  21810  flimopn  21826  fbflim2  21828  hausflimi  21831  hausflim  21832  flimcf  21833  flimclslem  21835  flimsncls  21837  hauspwpwf1  21838  cnpflfi  21850  fclsnei  21870  fclscf  21876  flimfnfcls  21879  fclscmp  21881  ufilcmp  21883  fcfnei  21886  cnpfcf  21892  alexsublem  21895  alexsub  21896  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem3  21905  ptcmplem4  21906  ptcmplem5  21907  symgtgp  21952  tgpconncompeqg  21962  tgpconncomp  21963  ghmcnp  21965  tgpt0  21969  qustgplem  21971  haustsms2  21987  tsmsgsum  21989  tsmsres  21994  tsmsxp  22005  imasdsf1olem  22225  xbln0  22266  blssps  22276  blss  22277  neibl  22353  blcld  22357  metss  22360  metequiv2  22362  met1stc  22373  metrest  22376  prdsxmslem2  22381  metcnp3  22392  nrmmetd  22426  nlmvscnlem1  22537  nrginvrcnlem  22542  nmoleub  22582  icccmplem2  22673  icccmp  22675  reconnlem2  22677  xrge0tsms  22684  metdstri  22701  metdseq0  22704  metdscn  22706  cnmpt2pc  22774  lebnumlem3  22809  pcoval2  22862  pcopt  22868  nmoleub2lem  22960  nmhmcn  22966  ipcnlem1  23090  cfilfcls  23118  cmetcaulem  23132  iscmet3lem2  23136  iscmet3  23137  equivcau  23144  caubl  23152  bcthlem2  23168  bcthlem3  23169  bcthlem4  23170  bcthlem5  23171  ivthlem2  23267  ivthlem3  23268  ovoliunlem2  23317  ovolicc2lem2  23332  ovolicc2lem3  23333  ovolicc2lem5  23335  ovolicc2  23336  ismbl2  23341  nulmbl  23349  nulmbl2  23350  unmbl  23351  shftmbl  23352  voliunlem3  23366  volsup  23370  ioombl1lem4  23375  ioombl1  23376  icombl  23378  ioombl  23379  uniioombl  23403  opnmbllem  23415  volivth  23421  vitali  23427  mbflimsup  23478  i1fadd  23507  itg1addlem4  23511  itg2le  23551  itg2seq  23554  itg2lea  23556  itg2splitlem  23560  itg2split  23561  itg2mono  23565  itg2gt0  23572  itg2cnlem2  23574  itgss  23623  itgfsum  23638  itgcn  23654  ellimc3  23688  limcco  23702  limciun  23703  dvnres  23739  dvnfre  23760  rolle  23798  c1liplem1  23804  dvivth  23818  dvne0  23819  lhop1lem  23821  lhop1  23822  lhop  23824  dvcnvrelem1  23825  dvfsumrlim  23839  dvfsum2  23842  ftc1a  23845  ftc1lem6  23849  itgsubst  23857  tdeglem4  23865  mdegaddle  23879  mdegvscale  23880  mdegmullem  23883  deg1tmle  23922  ply1divex  23941  dvdsq1p  23965  fta1g  23972  fta1b  23974  plyco0  23993  coeeulem  24025  dgrlem  24030  plyco  24042  coemullem  24051  dgreq0  24066  dgrco  24076  plydivex  24097  quotcan  24109  aannenlem1  24128  aalioulem2  24133  aalioulem3  24134  taylthlem1  24172  ulmbdd  24197  itgulm  24207  radcnvlt1  24217  psercnlem1  24224  abelthlem2  24231  abelthlem8  24238  logcnlem5  24437  efopn  24449  cxpmul2z  24482  cxpcn3lem  24533  cxpeq  24543  xrlimcnp  24740  cxplim  24743  o1cxp  24746  cxploglim  24749  scvxcvx  24757  jensen  24760  ftalem1  24844  ftalem2  24845  fta  24851  basellem3  24854  isppw2  24886  ppinprm  24923  chtnprm  24925  dvdsmulf1o  24965  chtublem  24981  perfectlem2  25000  dchrfi  25025  dchrptlem1  25034  dchrptlem2  25035  dchrptlem3  25036  dchrsum2  25038  bposlem1  25054  bposlem3  25056  2sqlem5  25192  2sqlem6  25193  2sqlem8  25196  2sqlem10  25198  2sqb  25202  chebbnd1lem1  25203  chtppilimlem2  25208  dchrisum0flb  25244  dchrisum0fno1  25245  dchrisum0  25254  pntrsumbnd2  25301  pntpbnd1  25320  pntpbnd2  25321  pntlemp  25344  pnt3  25346  qabvle  25359  ostth2lem2  25368  ostth3  25372  ostth  25373  colinearalglem4  25834  axcontlem10  25898  upgrex  26032  smcnlem  27680  ubthlem1  27854  ubthlem3  27856  htthlem  27902  5oalem6  28646  leopmuli  29120  pjnormssi  29155  pjclem4  29186  pj3si  29194  hatomistici  29349  sumdmdlem  29405  xrge0tsmsd  29913  isarchiofld  29945  ordtrest2NEWlem  30096  qqhf  30158  eulerpartlemb  30558  ballotlemfc0  30682  ballotlemfcc  30683  sgn3da  30731  subfacp1lem5  31292  erdszelem7  31305  erdszelem11  31309  pconnconn  31339  txpconn  31340  connpconn  31343  sconnpi1  31347  txsconn  31349  cvxsconn  31351  cvmopnlem  31386  cvmfolem  31387  cvmliftmolem2  31390  cvmliftlem7  31399  cvmliftlem10  31402  cvmlift2lem10  31420  cvmlift3lem4  31430  cvmlift3lem8  31434  msubff1  31579  frpomin  31863  wzel  31894  wsuclem  31895  nolt02o  31970  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  noetalem3  31990  btwnouttr2  32254  cgrxfr  32287  btwnxfr  32288  brcolinear  32291  lineext  32308  btwnconn1lem13  32331  midofsegid  32336  segcon2  32337  brsegle  32340  seglecgr12im  32342  segletr  32346  colinbtwnle  32350  broutsideof2  32354  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  outsideofeq  32362  outsideofeu  32363  outsidele  32364  lineunray  32379  lineelsb2  32380  linethru  32385  finminlem  32437  nn0prpwlem  32442  neibastop2lem  32480  neibastop2  32481  neibastop3  32482  topjoin  32485  tailfb  32497  relowlssretop  33341  wl-sbcom2d-lem1  33472  finixpnum  33524  poimirlem6  33545  poimirlem7  33546  poimirlem13  33552  poimirlem26  33565  poimirlem29  33568  heicant  33574  opnmbllem0  33575  mblfinlem3  33578  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  itg2addnclem3  33593  ftc1cnnc  33614  sdclem2  33668  fdc  33671  istotbnd3  33700  isbnd2  33712  isbnd3  33713  prdsbnd  33722  cntotbnd  33725  heibor1lem  33738  heibor1  33739  heiborlem10  33749  rrncmslem  33761  ghomco  33820  1idl  33955  unichnidl  33960  prtlem10  34469  prtlem18  34481  atlatmstc  34924  cvrexchlem  35023  paddasslem14  35437  pexmidlem5N  35578  cdleme29ex  35979  cdlemefr29exN  36007  cdleme32fva  36042  diarnN  36735  dihlsscpre  36840  isnacs3  37590  fnwe2lem2  37938  kelac1  37950  hbtlem5  38015  hbt  38017  dgraa0p  38036  monoordxrv  40025  rlimdmafv  41578  smonoord  41666  fmtnoprmfac2  41804  perfectALTVlem2  41956  mogoldbb  41998  mgmhmeql  42128  lindslinindsimp2  42577
  Copyright terms: Public domain W3C validator