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

Theorem expr 641
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 629 . 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 196  df-an 385
This theorem is referenced by:  reximddv  3001  rexlimdvaa  3014  disjxiun  4579  disjxiunOLD  4580  wereu2  5035  ordtr3  5686  fcof1  6442  knatar  6507  riota5f  6535  ovmpt2df  6690  extmptsuppeq  7206  suppss  7212  suppss2  7216  wfrlem17  7318  smoord  7349  tfrlem9a  7369  oaass  7528  oelimcl  7567  oaabs2  7612  swoso  7662  eceqoveq  7740  domdifsn  7928  domunsncan  7945  omxpenlem  7946  enfixsn  7954  mapdom2  8016  frfi  8090  fofinf1o  8126  finsschain  8156  elfiun  8219  marypha1lem  8222  eqsupd  8246  eqinfd  8274  ordiso2  8303  ordtypelem6  8311  ordtypelem7  8312  ordtypelem10  8315  oismo  8328  wemapsolem  8338  brwdom2  8361  wdomtr  8363  unwdomg  8372  xpwdomg  8373  unxpwdom2  8376  cantnfval2  8449  cantnfle  8451  cantnflem1  8469  cantnf  8473  r1ordg  8524  tcrank  8630  carddomi2  8679  harval2  8706  infxpenlem  8719  infxpenc2lem2  8726  fseqenlem1  8730  dfac8clem  8738  acndom2  8760  infpwfien  8768  iunfictbso  8820  dfac12lem3  8850  infxp  8920  coflim  8966  cofsmo  8974  coftr  8978  sornom  8982  infpssrlem4  9011  enfin2i  9026  fin23lem26  9030  fin23lem27  9033  fin23lem36  9053  fin23lem40  9056  isf32lem5  9062  isf34lem4  9082  isfin1-3  9091  fin1a2lem10  9114  fin1a2lem13  9117  fin1a2s  9119  hsmexlem4  9134  ttukeylem5  9218  ttukeylem6  9219  ttukeylem7  9220  alephval2  9273  gchor  9328  fpwwe2lem7  9337  fpwwe2lem12  9342  fpwwe2  9344  pwfseqlem4a  9362  pwfseqlem4  9363  winalim2  9397  gchina  9400  inar1  9476  nqereq  9636  prlem934  9734  prlem936  9748  addsrmo  9773  mulsrmo  9774  supsrlem  9811  axpre-sup  9869  dedekind  10079  dedekindle  10080  prodge0  10749  mulge0b  10772  supaddc  10867  supmul1  10869  un0addcl  11203  un0mulcl  11204  uzwo3  11659  qbtwnre  11904  xlemul1a  11990  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqf1olem1  12702  seqid2  12709  seqhomo  12710  expnegz  12756  expcan  12775  ltexp2  12776  discr  12863  bcval5  12967  hashbc  13094  hashf1lem2  13097  seqcoll  13105  seqcoll2  13106  wrdind  13328  wrd2ind  13329  cau3lem  13942  ello1d  14102  lo1bdd2  14103  rlimclim  14125  climrlim2  14126  rlimdm  14130  rlimcn1  14167  reccn2  14175  rlimsqzlem  14227  lo1le  14230  caucvgrlem  14251  caurcvg2  14256  summolem2  14294  zsum  14296  fsum  14298  fsumf1o  14301  sumss  14302  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  fsumcom2  14347  fsumcom2OLD  14348  fsum0diag2  14357  fsummulc2  14358  fsumconst  14364  fsumrelem  14380  fsumrlim  14384  fsumo1  14385  divrcnv  14423  geomulcvg  14446  mertenslem2  14456  prodmolem2  14504  zprod  14506  fprod  14510  fprodf1o  14515  prodss  14516  fprodss  14517  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodconst  14547  fprodn0  14548  fprodcom2  14553  fprodcom2OLD  14554  ruclem8  14805  dvds0lem  14830  dvdsnegb  14837  dvdssub2  14861  bitsf1  15006  bitsshft  15035  bezoutlem3  15096  bezoutlem4  15097  isprm2lem  15232  isprm5  15257  isprm6  15264  hashgcdeq  15332  modprminv  15342  modprminveq  15343  reumodprminv  15347  pcqmul  15396  pcqcl  15399  pcxcl  15403  pc2dvds  15421  pcadd  15431  pcmpt  15434  pockthg  15448  infpnlem1  15452  prmreclem5  15462  vdwlem2  15524  vdwlem9  15531  vdwlem10  15532  vdwlem12  15534  ramub  15555  0ram  15562  ramub1lem2  15569  ramub1  15570  ramcl  15571  mreexexd  16131  mreexexdOLD  16132  acsfn2  16147  iscatd  16157  catpropd  16192  setcmon  16560  pleval2i  16787  psss  17037  mgmidsssn0  17092  mhmeql  17187  frmdss2  17223  frmdup3  17227  grprcan  17278  dfgrp3lem  17336  mulgnn0ass  17401  isnsg3  17451  ghmpreima  17505  ghmeql  17506  gaorber  17564  f1omvdco2  17691  psgnunilem1  17736  psgnunilem2  17738  oddvds  17789  gexdvds  17822  sylow1lem1  17836  odcau  17842  pgpssslw  17852  sylow2alem2  17856  sylow2blem3  17860  fislw  17863  lsmmod  17911  efgredlem  17983  frgpup3  18014  gsumval3  18131  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  gsum2d2lem  18195  ablfac1eulem  18294  pgpfac1lem5  18301  ablfaclem3  18309  issubdrg  18628  lss1d  18784  lmhmeql  18876  lspextmo  18877  lspsnat  18966  lsppratlem6  18973  islbs3  18976  lbsextlem4  18982  lidl1el  19039  mvrf1  19246  mplsubglem  19255  mpllsslem  19256  mplcoe1  19286  mplcoe5  19289  gsummoncoe1  19495  cnsubrg  19625  gsumfsum  19632  prmirredlem  19660  znidomb  19729  frgpcyg  19741  cssmre  19856  dsmmsubg  19906  dsmmlss  19907  frlmsslsp  19954  lindff1  19978  lindfrn  19979  mat1dimcrng  20102  mdetdiaglem  20223  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  cpmatacl  20340  cpmatmcllem  20342  mp2pm2mplem4  20433  en2top  20600  toponmre  20707  topssnei  20738  innei  20739  clslp  20762  restcls  20795  restntr  20796  ordtrest2lem  20817  cnpco  20881  cncls2  20887  cncnpi  20892  cncnp  20894  cnconst2  20897  cnpdis  20907  lmcnp  20918  cnhaus  20968  isreg2  20991  cncmp  21005  tgcmp  21014  sscmp  21018  cmpfi  21021  cnconn  21035  iunconlem  21040  clscon  21043  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  2ndcdisj  21069  1stcelcls  21074  1stccnp  21075  restnlly  21095  cldllycmp  21108  lly1stc  21109  dislly  21110  locfincmp  21139  comppfsc  21145  kgentopon  21151  kgenidm  21160  1stckgenlem  21166  kgencn3  21171  ptpjpre1  21184  ptbasin  21190  txcls  21217  tx2cn  21223  ptpjcn  21224  ptclsg  21228  ptcnp  21235  txdis  21245  txlly  21249  txnlly  21250  pthaus  21251  txtube  21253  txcmplem1  21254  txcmplem2  21255  txcmp  21256  txhaus  21260  txkgen  21265  xkohaus  21266  xkococnlem  21272  xkococn  21273  txcon  21302  qtopeu  21329  qtoprest  21330  regr1lem2  21353  kqreglem1  21354  cmphaushmeo  21413  xkocnv  21427  fgabs  21493  filuni  21499  trufil  21524  ufileu  21533  filufint  21534  fin1aufil  21546  elfm2  21562  rnelfmlem  21566  fmfnfmlem2  21569  fmfnfmlem4  21571  fmufil  21573  flimopn  21589  fbflim2  21591  hausflimi  21594  hausflim  21595  flimcf  21596  flimclslem  21598  flimsncls  21600  hauspwpwf1  21601  cnpflfi  21613  fclsnei  21633  fclscf  21639  flimfnfcls  21642  fclscmp  21644  ufilcmp  21646  fcfnei  21649  cnpfcf  21655  alexsublem  21658  alexsub  21659  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem4  21669  ptcmplem5  21670  symgtgp  21715  tgpconcompeqg  21725  tgpconcomp  21726  ghmcnp  21728  tgpt0  21732  qustgplem  21734  haustsms2  21750  tsmsgsum  21752  tsmsres  21757  tsmsxp  21768  imasdsf1olem  21988  xbln0  22029  blssps  22039  blss  22040  neibl  22116  blcld  22120  metss  22123  metequiv2  22125  met1stc  22136  metrest  22139  prdsxmslem2  22144  metcnp3  22155  nrmmetd  22189  nlmvscnlem1  22300  nrginvrcnlem  22305  nmoleub  22345  icccmplem2  22434  icccmp  22436  reconnlem2  22438  xrge0tsms  22445  metdstri  22462  metdseq0  22465  metdscn  22467  cnmpt2pc  22535  lebnumlem3  22570  pcoval2  22624  pcopt  22630  nmoleub2lem  22722  nmhmcn  22728  ipcnlem1  22852  cfilfcls  22880  cmetcaulem  22894  iscmet3lem2  22898  iscmet3  22899  equivcau  22906  caubl  22914  bcthlem2  22930  bcthlem3  22931  bcthlem4  22932  bcthlem5  22933  ivthlem2  23028  ivthlem3  23029  ovoliunlem2  23078  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem5  23096  ovolicc2  23097  ismbl2  23102  nulmbl  23110  nulmbl2  23111  unmbl  23112  shftmbl  23113  voliunlem3  23127  volsup  23131  ioombl1lem4  23136  ioombl1  23137  icombl  23139  ioombl  23140  uniioombl  23163  opnmbllem  23175  volivth  23181  vitali  23188  mbflimsup  23239  i1fadd  23268  itg1addlem4  23272  itg2le  23312  itg2seq  23315  itg2lea  23317  itg2splitlem  23321  itg2split  23322  itg2mono  23326  itg2gt0  23333  itg2cnlem2  23335  itgss  23384  itgfsum  23399  itgcn  23415  ellimc3  23449  limcco  23463  limciun  23464  dvnres  23500  dvnfre  23521  rolle  23557  c1liplem1  23563  dvivth  23577  dvne0  23578  lhop1lem  23580  lhop1  23581  lhop  23583  dvcnvrelem1  23584  dvfsumrlim  23598  dvfsum2  23601  ftc1a  23604  ftc1lem6  23608  itgsubst  23616  tdeglem4  23624  mdegaddle  23638  mdegvscale  23639  mdegmullem  23642  deg1tmle  23681  ply1divex  23700  dvdsq1p  23724  fta1g  23731  fta1b  23733  plyco0  23752  coeeulem  23784  dgrlem  23789  plyco  23801  coemullem  23810  dgreq0  23825  dgrco  23835  plydivex  23856  quotcan  23868  aannenlem1  23887  aalioulem2  23892  aalioulem3  23893  taylthlem1  23931  ulmbdd  23956  itgulm  23966  radcnvlt1  23976  psercnlem1  23983  abelthlem2  23990  abelthlem8  23997  logcnlem5  24192  efopn  24204  cxpmul2z  24237  cxpcn3lem  24288  cxpeq  24298  xrlimcnp  24495  cxplim  24498  o1cxp  24501  cxploglim  24504  scvxcvx  24512  jensen  24515  ftalem1  24599  ftalem2  24600  fta  24606  basellem3  24609  isppw2  24641  ppinprm  24678  chtnprm  24680  dvdsmulf1o  24720  chtublem  24736  perfectlem2  24755  dchrfi  24780  dchrptlem1  24789  dchrptlem2  24790  dchrptlem3  24791  dchrsum2  24793  bposlem1  24809  bposlem3  24811  2sqlem5  24947  2sqlem6  24948  2sqlem8  24951  2sqlem10  24953  2sqb  24957  chebbnd1lem1  24958  chtppilimlem2  24963  dchrisum0flb  24999  dchrisum0fno1  25000  dchrisum0  25009  pntrsumbnd2  25056  pntpbnd1  25075  pntpbnd2  25076  pntlemp  25099  pnt3  25101  qabvle  25114  ostth2lem2  25123  ostth3  25127  ostth  25128  colinearalglem4  25589  axcontlem10  25653  upgrex  25759  umgraex  25852  eupai  26494  numclwwlkovf2ex  26613  smcnlem  26936  ubthlem1  27110  ubthlem3  27112  htthlem  27158  5oalem6  27902  leopmuli  28376  pjnormssi  28411  pjclem4  28442  pj3si  28450  hatomistici  28605  sumdmdlem  28661  xrge0tsmsd  29116  isarchiofld  29148  ordtrest2NEWlem  29296  qqhf  29358  eulerpartlemb  29757  ballotlemfc0  29881  ballotlemfcc  29882  sgn3da  29930  subfacp1lem5  30420  erdszelem7  30433  erdszelem11  30437  pconcon  30467  txpcon  30468  conpcon  30471  sconpi1  30475  txscon  30477  cvxscon  30479  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem10  30548  cvmlift3lem4  30558  cvmlift3lem8  30562  msubff1  30707  wzel  31015  wzelOLD  31016  wsuclem  31017  wsuclemOLD  31018  nofulllem4  31104  btwnouttr2  31299  cgrxfr  31332  btwnxfr  31333  brcolinear  31336  lineext  31353  btwnconn1lem13  31376  midofsegid  31381  segcon2  31382  brsegle  31385  seglecgr12im  31387  segletr  31391  colinbtwnle  31395  broutsideof2  31399  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsideofeq  31407  outsideofeu  31408  outsidele  31409  lineunray  31424  lineelsb2  31425  linethru  31430  finminlem  31482  nn0prpwlem  31487  neibastop2lem  31525  neibastop2  31526  neibastop3  31527  topjoin  31530  tailfb  31542  relowlssretop  32387  wl-sbcom2d-lem1  32521  finixpnum  32564  poimirlem6  32585  poimirlem7  32586  poimirlem13  32592  poimirlem26  32605  poimirlem29  32608  heicant  32614  opnmbllem0  32615  mblfinlem3  32618  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  itg2addnclem3  32633  ftc1cnnc  32654  sdclem2  32708  fdc  32711  istotbnd3  32740  isbnd2  32752  isbnd3  32753  prdsbnd  32762  cntotbnd  32765  heibor1lem  32778  heibor1  32779  heiborlem10  32789  rrncmslem  32801  ghomco  32860  1idl  32995  unichnidl  33000  prtlem10  33168  prtlem18  33180  atlatmstc  33624  cvrexchlem  33723  paddasslem14  34137  pexmidlem5N  34278  cdleme29ex  34680  cdlemefr29exN  34708  cdleme32fva  34743  diarnN  35436  dihlsscpre  35541  isnacs3  36291  fnwe2lem2  36639  kelac1  36651  hbtlem5  36717  hbt  36719  dgraa0p  36738  rlimdmafv  39906  smonoord  39944  fmtnoprmfac2  40017  perfectALTVlem2  40165  av-numclwwlkovf2ex  41517  mgmhmeql  41593  lindslinindsimp2  42046
  Copyright terms: Public domain W3C validator