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

Theorem expr 446
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 409 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 395 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  animpimp2impd  864  3expia  1143  reximddv  3205  rexlimdvaa  3220  disjxiun  4841  wereu2  5308  ordtr3  5982  fcof1  6766  knatar  6831  riota5f  6860  ovmpt2df  7022  extmptsuppeq  7553  suppss  7560  suppss2  7564  wfrlem17  7667  smoord  7698  tfrlem9a  7718  oaass  7878  oelimcl  7917  oaabs2  7962  swoso  8012  eceqoveq  8088  domdifsn  8282  domunsncan  8299  omxpenlem  8300  enfixsn  8308  mapdom2  8370  frfi  8444  fofinf1o  8480  finsschain  8512  elfiun  8575  marypha1lem  8578  eqsupd  8602  eqinfd  8630  ordiso2  8659  ordtypelem6  8667  ordtypelem7  8668  ordtypelem10  8671  oismo  8684  wemapsolem  8694  brwdom2  8717  wdomtr  8719  unwdomg  8728  xpwdomg  8729  unxpwdom2  8732  cantnfval2  8813  cantnfle  8815  cantnflem1  8833  cantnf  8837  r1ordg  8888  tcrank  8994  carddomi2  9079  harval2  9106  infxpenlem  9119  infxpenc2lem2  9126  fseqenlem1  9130  dfac8clem  9138  acndom2  9160  infpwfien  9168  iunfictbso  9220  dfac12lem3  9252  infxp  9322  coflim  9368  cofsmo  9376  coftr  9380  sornom  9384  infpssrlem4  9413  enfin2i  9428  fin23lem26  9432  fin23lem27  9435  fin23lem36  9455  fin23lem40  9458  isf32lem5  9464  isf34lem4  9484  isfin1-3  9493  fin1a2lem10  9516  fin1a2lem13  9519  fin1a2s  9521  hsmexlem4  9536  ttukeylem5  9620  ttukeylem6  9621  ttukeylem7  9622  alephval2  9679  gchor  9734  fpwwe2lem7  9743  fpwwe2lem12  9748  fpwwe2  9750  pwfseqlem4a  9768  pwfseqlem4  9769  winalim2  9803  gchina  9806  inar1  9882  nqereq  10042  prlem934  10140  prlem936  10154  addsrmo  10179  mulsrmo  10180  supsrlem  10217  axpre-sup  10275  dedekind  10485  dedekindle  10486  prodge0OLD  11155  mulge0b  11178  supaddc  11275  supmul1  11277  un0addcl  11592  un0mulcl  11593  uzwo3  12002  qbtwnre  12248  xlemul1a  12336  seqcl2  13042  seqfveq2  13046  seqshft2  13050  monoord  13054  seqsplit  13057  seqf1olem1  13063  seqid2  13070  seqhomo  13071  expnegz  13117  expcan  13136  ltexp2  13137  discr  13224  bcval5  13325  hashbc  13454  hashf1lem2  13457  seqcoll  13465  seqcoll2  13466  wrdind  13700  wrd2ind  13701  cau3lem  14317  ello1d  14477  lo1bdd2  14478  rlimclim  14500  climrlim2  14501  rlimdm  14505  rlimcn1  14542  reccn2  14550  rlimsqzlem  14602  lo1le  14605  caucvgrlem  14626  caurcvg2  14631  summolem2  14670  zsum  14672  fsum  14674  fsumf1o  14677  sumss  14678  fsumss  14679  fsumcl2lem  14685  fsumadd  14693  fsumcom2  14728  fsum0diag2  14737  fsummulc2  14738  fsumconst  14744  fsumrelem  14761  fsumrlim  14765  fsumo1  14766  divrcnv  14806  geomulcvg  14829  mertenslem2  14838  prodmolem2  14886  zprod  14888  fprod  14892  fprodf1o  14897  prodss  14898  fprodss  14899  fprodcl2lem  14901  fprodmul  14911  fproddiv  14912  fprodconst  14929  fprodn0  14930  fprodcom2  14935  ruclem8  15186  dvds0lem  15215  dvdsnegb  15222  dvdssub2  15246  bitsf1  15387  bitsshft  15416  bezoutlem3  15477  bezoutlem4  15478  isprm5  15636  isprm6  15643  hashgcdeq  15711  modprminv  15721  modprminveq  15722  reumodprminv  15726  pcqmul  15775  pcqcl  15778  pcxcl  15782  pc2dvds  15800  pcadd  15810  pcmpt  15813  pockthg  15827  infpnlem1  15831  prmreclem5  15841  vdwlem2  15903  vdwlem9  15910  vdwlem10  15911  vdwlem12  15913  ramub  15934  0ram  15941  ramub1lem2  15948  ramub1  15949  ramcl  15950  mreexexd  16513  acsfn2  16528  iscatd  16538  catpropd  16573  setcmon  16941  pleval2i  17169  psss  17419  mgmidsssn0  17474  mhmeql  17569  frmdss2  17605  frmdup3  17609  grprcan  17660  dfgrp3lem  17718  mulgnn0ass  17780  isnsg3  17830  ghmpreima  17884  ghmeql  17885  gaorber  17942  f1omvdco2  18069  psgnunilem1  18114  psgnunilem2  18116  oddvds  18167  gexdvds  18200  sylow1lem1  18214  odcau  18220  pgpssslw  18230  sylow2alem2  18234  sylow2blem3  18238  fislw  18241  lsmmod  18289  efgredlem  18361  frgpup3  18392  gsumval3  18509  gsumzres  18511  gsumzcl2  18512  gsumzf1o  18514  gsumzaddlem  18522  gsumconst  18535  gsumzmhm  18538  gsumzoppg  18545  gsum2d2lem  18573  ablfac1eulem  18673  pgpfac1lem5  18680  ablfaclem3  18688  issubdrg  19009  lss1d  19170  lmhmeql  19262  lspextmo  19263  lspsnat  19353  lsppratlem6  19361  islbs3  19364  lbsextlem4  19370  lidl1el  19427  mvrf1  19634  mplsubglem  19643  mpllsslem  19644  mplcoe1  19674  mplcoe5  19677  gsummoncoe1  19882  cnsubrg  20014  gsumfsum  20021  prmirredlem  20049  znidomb  20117  frgpcyg  20129  cssmre  20247  dsmmsubg  20297  dsmmlss  20298  frlmsslsp  20345  lindff1  20369  lindfrn  20370  mat1dimcrng  20494  mdetdiaglem  20615  mdetunilem7  20635  mdetunilem8  20636  mdetunilem9  20637  cpmatacl  20734  cpmatmcllem  20736  mp2pm2mplem4  20827  en2top  21003  toponmre  21111  topssnei  21142  innei  21143  clslp  21166  restcls  21199  restntr  21200  ordtrest2lem  21221  cnpco  21285  cncls2  21291  cncnpi  21296  cncnp  21298  cnconst2  21301  cnpdis  21311  lmcnp  21322  cnhaus  21372  isreg2  21395  cncmp  21409  tgcmp  21418  sscmp  21422  cmpfi  21425  cnconn  21439  iunconnlem  21444  clsconn  21447  1stcfb  21462  1stcrest  21470  2ndcctbss  21472  2ndcdisj  21473  1stcelcls  21478  1stccnp  21479  restnlly  21499  cldllycmp  21512  lly1stc  21513  dislly  21514  locfincmp  21543  comppfsc  21549  kgentopon  21555  kgenidm  21564  1stckgenlem  21570  kgencn3  21575  ptpjpre1  21588  ptbasin  21594  txcls  21621  tx2cn  21627  ptpjcn  21628  ptclsg  21632  ptcnp  21639  txdis  21649  txlly  21653  txnlly  21654  pthaus  21655  txtube  21657  txcmplem1  21658  txcmplem2  21659  txcmp  21660  txhaus  21664  txkgen  21669  xkohaus  21670  xkococnlem  21676  xkococn  21677  txconn  21706  qtopeu  21733  qtoprest  21734  regr1lem2  21757  kqreglem1  21758  cmphaushmeo  21817  xkocnv  21831  fgabs  21896  filuni  21902  trufil  21927  ufileu  21936  filufint  21937  fin1aufil  21949  elfm2  21965  rnelfmlem  21969  fmfnfmlem2  21972  fmfnfmlem4  21974  fmufil  21976  flimopn  21992  fbflim2  21994  hausflimi  21997  hausflim  21998  flimcf  21999  flimclslem  22001  flimsncls  22003  hauspwpwf1  22004  cnpflfi  22016  fclsnei  22036  fclscf  22042  flimfnfcls  22045  fclscmp  22047  ufilcmp  22049  fcfnei  22052  cnpfcf  22058  alexsublem  22061  alexsub  22062  alexsubALTlem2  22065  alexsubALTlem3  22066  alexsubALTlem4  22067  ptcmplem3  22071  ptcmplem4  22072  ptcmplem5  22073  symgtgp  22118  tgpconncompeqg  22128  tgpconncomp  22129  ghmcnp  22131  tgpt0  22135  qustgplem  22137  haustsms2  22153  tsmsgsum  22155  tsmsres  22160  tsmsxp  22171  imasdsf1olem  22391  xbln0  22432  blssps  22442  blss  22443  neibl  22519  blcld  22523  metss  22526  metequiv2  22528  met1stc  22539  metrest  22542  prdsxmslem2  22547  metcnp3  22558  nrmmetd  22592  nlmvscnlem1  22703  nrginvrcnlem  22708  nmoleub  22748  icccmplem2  22839  icccmp  22841  reconnlem2  22843  xrge0tsms  22850  metdstri  22867  metdseq0  22870  metdscn  22872  cnmpt2pc  22940  lebnumlem3  22975  pcoval2  23028  pcopt  23034  nmoleub2lem  23126  nmhmcn  23132  ipcnlem1  23256  cfilfcls  23284  cmetcaulem  23298  iscmet3lem2  23302  iscmet3  23303  equivcau  23310  caubl  23318  bcthlem2  23334  bcthlem3  23335  bcthlem4  23336  bcthlem5  23337  ivthlem2  23433  ivthlem3  23434  ovoliunlem2  23484  ovolicc2lem2  23499  ovolicc2lem5  23502  ovolicc2  23503  ismbl2  23508  nulmbl  23516  nulmbl2  23517  unmbl  23518  shftmbl  23519  voliunlem3  23533  volsup  23537  ioombl1lem4  23542  ioombl1  23543  icombl  23545  ioombl  23546  uniioombl  23570  opnmbllem  23582  volivth  23588  vitali  23594  mbflimsup  23647  i1fadd  23676  itg1addlem4  23680  itg2le  23720  itg2seq  23723  itg2lea  23725  itg2splitlem  23729  itg2split  23730  itg2mono  23734  itg2gt0  23741  itg2cnlem2  23743  itgss  23792  itgfsum  23807  itgcn  23823  ellimc3  23857  limcco  23871  limciun  23872  dvnres  23908  dvnfre  23929  rolle  23967  c1liplem1  23973  dvivth  23987  dvne0  23988  lhop1lem  23990  lhop1  23991  lhop  23993  dvcnvrelem1  23994  dvfsumrlim  24008  dvfsum2  24011  ftc1a  24014  ftc1lem6  24018  itgsubst  24026  tdeglem4  24034  mdegaddle  24048  mdegvscale  24049  mdegmullem  24052  deg1tmle  24091  ply1divex  24110  dvdsq1p  24134  fta1g  24141  fta1b  24143  plyco0  24162  coeeulem  24194  dgrlem  24199  plyco  24211  coemullem  24220  dgreq0  24235  dgrco  24245  plydivex  24266  quotcan  24278  aannenlem1  24297  aalioulem2  24302  aalioulem3  24303  taylthlem1  24341  ulmbdd  24366  itgulm  24376  radcnvlt1  24386  psercnlem1  24393  abelthlem2  24400  abelthlem8  24407  logcnlem5  24606  efopn  24618  cxpmul2z  24651  cxpcn3lem  24702  cxpeq  24712  xrlimcnp  24909  cxplim  24912  o1cxp  24915  cxploglim  24918  scvxcvx  24926  jensen  24929  ftalem1  25013  ftalem2  25014  fta  25020  basellem3  25023  isppw2  25055  ppinprm  25092  chtnprm  25094  dvdsmulf1o  25134  chtublem  25150  perfectlem2  25169  dchrfi  25194  dchrptlem1  25203  dchrptlem2  25204  dchrptlem3  25205  dchrsum2  25207  bposlem1  25223  bposlem3  25225  2sqlem5  25361  2sqlem6  25362  2sqlem8  25365  2sqlem10  25367  2sqb  25371  chebbnd1lem1  25372  chtppilimlem2  25377  dchrisum0flb  25413  dchrisum0fno1  25414  dchrisum0  25423  pntrsumbnd2  25470  pntpbnd1  25489  pntpbnd2  25490  pntlemp  25513  pnt3  25515  qabvle  25528  ostth2lem2  25537  ostth3  25541  ostth  25542  colinearalglem4  26003  axcontlem10  26067  upgrex  26201  smcnlem  27880  ubthlem1  28054  ubthlem3  28056  htthlem  28102  5oalem6  28846  leopmuli  29320  pjnormssi  29355  pjclem4  29386  pj3si  29394  hatomistici  29549  sumdmdlem  29605  xrge0tsmsd  30110  isarchiofld  30142  ordtrest2NEWlem  30293  qqhf  30355  eulerpartlemb  30755  ballotlemfc0  30879  ballotlemfcc  30880  sgn3da  30928  subfacp1lem5  31489  erdszelem7  31502  erdszelem11  31506  pconnconn  31536  txpconn  31537  connpconn  31540  sconnpi1  31544  txsconn  31546  cvxsconn  31548  cvmopnlem  31583  cvmfolem  31584  cvmliftmolem2  31587  cvmliftlem7  31596  cvmliftlem10  31599  cvmlift2lem10  31617  cvmlift3lem4  31627  cvmlift3lem8  31631  msubff1  31776  frpomin  32059  wzel  32090  wsuclem  32091  nolt02o  32166  nosupbnd1lem3  32177  nosupbnd1lem4  32178  nosupbnd1lem5  32179  noetalem3  32186  btwnouttr2  32450  cgrxfr  32483  btwnxfr  32484  brcolinear  32487  lineext  32504  btwnconn1lem13  32527  midofsegid  32532  segcon2  32533  brsegle  32536  seglecgr12im  32538  segletr  32542  colinbtwnle  32546  broutsideof2  32550  btwnoutside  32553  broutsideof3  32554  outsideoftr  32557  outsideofeq  32558  outsideofeu  32559  outsidele  32560  lineunray  32575  lineelsb2  32576  linethru  32581  finminlem  32633  nn0prpwlem  32638  neibastop2lem  32676  neibastop2  32677  neibastop3  32678  topjoin  32681  tailfb  32693  relowlssretop  33527  wl-sbcom2d-lem1  33656  finixpnum  33707  poimirlem6  33728  poimirlem7  33729  poimirlem13  33735  poimirlem26  33748  poimirlem29  33751  heicant  33757  opnmbllem0  33758  mblfinlem3  33761  ismblfin  33763  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  itg2addnclem  33773  itg2addnclem3  33775  ftc1cnnc  33796  sdclem2  33849  fdc  33852  istotbnd3  33881  isbnd2  33893  isbnd3  33894  prdsbnd  33903  cntotbnd  33906  heibor1lem  33919  heibor1  33920  heiborlem10  33930  rrncmslem  33942  ghomco  34001  1idl  34136  unichnidl  34141  prtlem10  34644  prtlem18  34656  atlatmstc  35099  cvrexchlem  35199  paddasslem14  35613  pexmidlem5N  35754  cdleme29ex  36155  cdlemefr29exN  36183  cdleme32fva  36218  diarnN  36910  dihlsscpre  37015  isnacs3  37775  fnwe2lem2  38122  kelac1  38134  hbtlem5  38199  hbt  38201  dgraa0p  38220  monoordxrv  40191  rlimdmafv  41766  rlimdmafv2  41847  fmtnoprmfac2  42054  perfectALTVlem2  42206  mogoldbb  42248  mgmhmeql  42371  lindslinindsimp2  42820
  Copyright terms: Public domain W3C validator