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

Theorem expr 457
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 421 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 407 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  animpimp2impd  842  3expia  1115  reximddv  3280  rexlimdvaa  3290  disjxiun  5060  wereu2  5551  ordtr3  6235  fcof1  7039  knatar  7104  riota5f  7136  ovmpodf  7300  extmptsuppeq  7850  suppss  7856  suppss2  7860  wfrlem17  7967  smoord  7998  tfrlem9a  8018  oaass  8182  oelimcl  8221  oaabs2  8267  swoso  8317  eceqoveq  8397  domdifsn  8594  domunsncan  8611  omxpenlem  8612  enfixsn  8620  mapdom2  8682  frfi  8757  fofinf1o  8793  finsschain  8825  elfiun  8888  marypha1lem  8891  eqsupd  8915  eqinfd  8943  ordiso2  8973  ordtypelem6  8981  ordtypelem7  8982  ordtypelem10  8985  oismo  8998  wemapsolem  9008  brwdom2  9031  wdomtr  9033  unwdomg  9042  xpwdomg  9043  unxpwdom2  9046  cantnfval2  9126  cantnfle  9128  cantnflem1  9146  cantnf  9150  r1ordg  9201  tcrank  9307  carddomi2  9393  harval2  9420  infxpenlem  9433  infxpenc2lem2  9440  fseqenlem1  9444  dfac8clem  9452  acndom2  9474  infpwfien  9482  iunfictbso  9534  dfac12lem3  9565  infxp  9631  coflim  9677  cofsmo  9685  coftr  9689  sornom  9693  infpssrlem4  9722  enfin2i  9737  fin23lem26  9741  fin23lem27  9744  fin23lem36  9764  fin23lem40  9767  isf32lem5  9773  isf34lem4  9793  isfin1-3  9802  fin1a2lem10  9825  fin1a2lem13  9828  fin1a2s  9830  hsmexlem4  9845  ttukeylem5  9929  ttukeylem6  9930  ttukeylem7  9931  alephval2  9988  gchor  10043  fpwwe2lem7  10052  fpwwe2lem12  10057  fpwwe2  10059  pwfseqlem4a  10077  pwfseqlem4  10078  winalim2  10112  gchina  10115  inar1  10191  nqereq  10351  prlem934  10449  prlem936  10463  addsrmo  10489  mulsrmo  10490  supsrlem  10527  axpre-sup  10585  dedekind  10797  dedekindle  10798  mulge0b  11504  supaddc  11602  supmul1  11604  un0addcl  11924  un0mulcl  11925  uzwo3  12337  qbtwnre  12587  xlemul1a  12676  seqcl2  13383  seqfveq2  13387  seqshft2  13391  monoord  13395  seqsplit  13398  seqf1olem1  13404  seqid2  13411  seqhomo  13412  expnegz  13458  expcan  13528  ltexp2  13529  discr  13596  bcval5  13673  hashbc  13806  hashf1lem2  13809  seqcoll  13817  seqcoll2  13818  wrdind  14079  wrd2ind  14080  cau3lem  14709  ello1d  14875  lo1bdd2  14876  rlimclim  14898  climrlim2  14899  rlimdm  14903  rlimcn1  14940  reccn2  14948  rlimsqzlem  15000  lo1le  15003  caucvgrlem  15024  caurcvg2  15029  summolem2  15068  zsum  15070  fsum  15072  fsumf1o  15075  sumss  15076  fsumss  15077  fsumcl2lem  15083  fsumadd  15091  fsumcom2  15124  fsum0diag2  15133  fsummulc2  15134  fsumconst  15140  fsumrelem  15157  fsumrlim  15161  fsumo1  15162  divrcnv  15202  geomulcvg  15227  mertenslem2  15236  prodmolem2  15284  zprod  15286  fprod  15290  fprodf1o  15295  prodss  15296  fprodss  15297  fprodcl2lem  15299  fprodmul  15309  fproddiv  15310  fprodconst  15327  fprodn0  15328  fprodcom2  15333  ruclem8  15585  dvds0lem  15615  dvdsnegb  15622  dvdssub2  15646  bitsf1  15790  bitsshft  15819  bezoutlem3  15884  bezoutlem4  15885  isprm5  16046  isprm6  16053  hashgcdeq  16121  modprminv  16131  modprminveq  16132  reumodprminv  16136  pcqmul  16185  pcqcl  16188  pcxcl  16192  pc2dvds  16210  pcadd  16220  pcmpt  16223  pockthg  16237  infpnlem1  16241  prmreclem5  16251  vdwlem2  16313  vdwlem9  16320  vdwlem10  16321  vdwlem12  16323  ramub  16344  0ram  16351  ramub1lem2  16358  ramub1  16359  ramcl  16360  mreexexd  16914  acsfn2  16929  iscatd  16939  catpropd  16974  setcmon  17342  pleval2i  17569  psss  17819  mgmidsssn0  17877  mhmeql  17985  frmdss2  18023  frmdup3  18027  grprcan  18082  dfgrp3lem  18142  mulgnn0ass  18208  isnsg3  18257  ghmpreima  18325  ghmeql  18326  gaorber  18383  f1omvdco2  18512  psgnunilem1  18557  psgnunilem2  18559  oddvds  18611  gexdvds  18645  sylow1lem1  18659  odcau  18665  pgpssslw  18675  sylow2alem2  18679  sylow2blem3  18683  fislw  18686  lsmmod  18737  efgredlem  18809  frgpup3  18840  gsumval3  18963  gsumzres  18965  gsumzcl2  18966  gsumzf1o  18968  gsumzaddlem  18977  gsumconst  18990  gsumzmhm  18993  gsumzoppg  19000  gsum2d2lem  19029  ablfac1eulem  19130  pgpfac1lem5  19137  ablfaclem3  19145  issubdrg  19496  lss1d  19671  lmhmeql  19763  lspextmo  19764  lspsnat  19853  lsppratlem6  19860  islbs3  19863  lbsextlem4  19869  lidl1el  19926  rnasclassa  20059  mvrf1  20140  mplsubglem  20149  mpllsslem  20150  mplcoe1  20181  mplcoe5  20184  gsummoncoe1  20407  cnsubrg  20540  gsumfsum  20547  prmirredlem  20575  znidomb  20643  frgpcyg  20655  cssmre  20772  dsmmsubg  20822  dsmmlss  20823  frlmsslsp  20875  lindff1  20899  lindfrn  20900  mat1dimcrng  21021  mdetdiaglem  21142  mdetunilem7  21162  mdetunilem8  21163  mdetunilem9  21164  cpmatacl  21259  cpmatmcllem  21261  mp2pm2mplem4  21352  en2top  21528  toponmre  21636  topssnei  21667  innei  21668  clslp  21691  restcls  21724  restntr  21725  ordtrest2lem  21746  cnpco  21810  cncls2  21816  cncnpi  21821  cncnp  21823  cnconst2  21826  cnpdis  21836  lmcnp  21847  cnhaus  21897  isreg2  21920  cncmp  21935  tgcmp  21944  sscmp  21948  cmpfi  21951  cnconn  21965  iunconnlem  21970  clsconn  21973  1stcfb  21988  1stcrest  21996  2ndcctbss  21998  2ndcdisj  21999  1stcelcls  22004  1stccnp  22005  restnlly  22025  cldllycmp  22038  lly1stc  22039  dislly  22040  locfincmp  22069  comppfsc  22075  kgentopon  22081  kgenidm  22090  1stckgenlem  22096  kgencn3  22101  ptpjpre1  22114  ptbasin  22120  txcls  22147  tx2cn  22153  ptpjcn  22154  ptclsg  22158  ptcnp  22165  txdis  22175  txlly  22179  txnlly  22180  pthaus  22181  txtube  22183  txcmplem1  22184  txcmplem2  22185  txcmp  22186  txhaus  22190  txkgen  22195  xkohaus  22196  xkococnlem  22202  xkococn  22203  txconn  22232  qtopeu  22259  qtoprest  22260  regr1lem2  22283  kqreglem1  22284  cmphaushmeo  22343  xkocnv  22357  fgabs  22422  filuni  22428  trufil  22453  ufileu  22462  filufint  22463  fin1aufil  22475  elfm2  22491  rnelfmlem  22495  fmfnfmlem2  22498  fmfnfmlem4  22500  fmufil  22502  flimopn  22518  fbflim2  22520  hausflimi  22523  hausflim  22524  flimcf  22525  flimclslem  22527  flimsncls  22529  hauspwpwf1  22530  cnpflfi  22542  fclsnei  22562  fclscf  22568  flimfnfcls  22571  fclscmp  22573  ufilcmp  22575  fcfnei  22578  cnpfcf  22584  alexsublem  22587  alexsub  22588  alexsubALTlem2  22591  alexsubALTlem3  22592  alexsubALTlem4  22593  ptcmplem3  22597  ptcmplem4  22598  ptcmplem5  22599  symgtgp  22644  tgpconncompeqg  22654  tgpconncomp  22655  ghmcnp  22657  tgpt0  22661  qustgplem  22663  haustsms2  22679  tsmsgsum  22681  tsmsres  22686  tsmsxp  22697  imasdsf1olem  22917  xbln0  22958  blssps  22968  blss  22969  neibl  23045  blcld  23049  metss  23052  metequiv2  23054  met1stc  23065  metrest  23068  prdsxmslem2  23073  metcnp3  23084  nrmmetd  23118  nlmvscnlem1  23229  nrginvrcnlem  23234  nmoleub  23274  icccmplem2  23365  icccmp  23367  reconnlem2  23369  xrge0tsms  23376  metdstri  23393  metdseq0  23396  metdscn  23398  cnmpopc  23466  lebnumlem3  23501  pcoval2  23554  pcopt  23560  nmoleub2lem  23652  nmhmcn  23658  ipcnlem1  23782  cfilfcls  23811  cmetcaulem  23825  iscmet3lem2  23829  iscmet3  23830  equivcau  23837  caubl  23845  bcthlem2  23862  bcthlem3  23863  bcthlem4  23864  bcthlem5  23865  ivthlem2  23987  ivthlem3  23988  ovoliunlem2  24038  ovolicc2lem2  24053  ovolicc2lem5  24056  ovolicc2  24057  ismbl2  24062  nulmbl  24070  nulmbl2  24071  unmbl  24072  shftmbl  24073  voliunlem3  24087  volsup  24091  ioombl1lem4  24096  ioombl1  24097  icombl  24099  ioombl  24100  uniioombl  24124  opnmbllem  24136  volivth  24142  vitali  24148  mbflimsup  24201  i1fadd  24230  itg1addlem4  24234  itg2le  24274  itg2seq  24277  itg2lea  24279  itg2splitlem  24283  itg2split  24284  itg2mono  24288  itg2gt0  24295  itg2cnlem2  24297  itgss  24346  itgfsum  24361  itgcn  24377  ellimc3  24411  limcco  24425  limciun  24426  dvnres  24462  dvnfre  24483  rolle  24521  c1liplem1  24527  dvivth  24541  dvne0  24542  lhop1lem  24544  lhop1  24545  lhop  24547  dvcnvrelem1  24548  dvfsumrlim  24562  dvfsum2  24565  ftc1a  24568  ftc1lem6  24572  itgsubst  24580  tdeglem4  24588  mdegaddle  24602  mdegvscale  24603  mdegmullem  24606  deg1tmle  24645  ply1divex  24664  dvdsq1p  24688  fta1g  24695  fta1b  24697  plyco0  24716  coeeulem  24748  dgrlem  24753  plyco  24765  coemullem  24774  dgreq0  24789  dgrco  24799  plydivex  24820  quotcan  24832  aannenlem1  24851  aalioulem2  24856  aalioulem3  24857  taylthlem1  24895  ulmbdd  24920  itgulm  24930  radcnvlt1  24940  psercnlem1  24947  abelthlem2  24954  abelthlem8  24961  logcnlem5  25161  efopn  25173  cxpmul2z  25206  cxpcn3lem  25260  cxpeq  25270  xrlimcnp  25479  cxplim  25482  o1cxp  25485  cxploglim  25488  scvxcvx  25496  jensen  25499  ftalem1  25583  ftalem2  25584  fta  25590  basellem3  25593  isppw2  25625  ppinprm  25662  chtnprm  25664  dvdsmulf1o  25704  chtublem  25720  perfectlem2  25739  dchrfi  25764  dchrptlem1  25773  dchrptlem2  25774  dchrptlem3  25775  dchrsum2  25777  bposlem1  25793  bposlem3  25795  2sqlem5  25931  2sqlem6  25932  2sqlem8  25935  2sqlem10  25937  2sqb  25941  chebbnd1lem1  25978  chtppilimlem2  25983  dchrisum0flb  26019  dchrisum0fno1  26020  dchrisum0  26029  pntrsumbnd2  26076  pntpbnd1  26095  pntpbnd2  26096  pntlemp  26119  pnt3  26121  qabvle  26134  ostth2lem2  26143  ostth3  26147  ostth  26148  colinearalglem4  26628  axcontlem10  26692  upgrex  26810  smcnlem  28407  ubthlem1  28580  ubthlem3  28582  htthlem  28627  5oalem6  29369  leopmuli  29843  pjnormssi  29878  pjclem4  29909  pj3si  29917  hatomistici  30072  sumdmdlem  30128  wrdt2ind  30560  xrge0tsmsd  30625  isarchiofld  30823  ordtrest2NEWlem  31070  qqhf  31132  eulerpartlemb  31531  ballotlemfc0  31655  ballotlemfcc  31656  sgn3da  31704  subfacp1lem5  32334  erdszelem7  32347  erdszelem11  32351  pconnconn  32381  txpconn  32382  connpconn  32385  sconnpi1  32389  txsconn  32391  cvxsconn  32393  cvmopnlem  32428  cvmfolem  32429  cvmliftmolem2  32432  cvmliftlem7  32441  cvmliftlem10  32444  cvmlift2lem10  32462  cvmlift3lem4  32472  cvmlift3lem8  32476  satfun  32561  msubff1  32706  frpomin  32981  wzel  33014  wsuclem  33015  frrlem14  33039  nolt02o  33102  nosupbnd1lem3  33113  nosupbnd1lem4  33114  nosupbnd1lem5  33115  noetalem3  33122  btwnouttr2  33386  cgrxfr  33419  btwnxfr  33420  brcolinear  33423  lineext  33440  btwnconn1lem13  33463  midofsegid  33468  segcon2  33469  brsegle  33472  seglecgr12im  33474  segletr  33478  colinbtwnle  33482  broutsideof2  33486  btwnoutside  33489  broutsideof3  33490  outsideoftr  33493  outsideofeq  33494  outsideofeu  33495  outsidele  33496  lineunray  33511  lineelsb2  33512  linethru  33517  finminlem  33569  nn0prpwlem  33573  neibastop2lem  33611  neibastop2  33612  neibastop3  33613  topjoin  33616  tailfb  33628  relowlssretop  34532  fvineqsneq  34581  wl-sbcom2d-lem1  34681  finixpnum  34763  poimirlem6  34784  poimirlem7  34785  poimirlem13  34791  poimirlem26  34804  poimirlem29  34807  heicant  34813  opnmbllem0  34814  mblfinlem3  34817  ismblfin  34819  ovoliunnfl  34820  voliunnfl  34822  volsupnfl  34823  itg2addnclem  34829  itg2addnclem3  34831  ftc1cnnc  34852  sdclem2  34904  fdc  34907  istotbnd3  34936  isbnd2  34948  isbnd3  34949  prdsbnd  34958  cntotbnd  34961  heibor1lem  34974  heibor1  34975  heiborlem10  34985  rrncmslem  34997  ghomco  35056  1idl  35191  unichnidl  35196  prtlem10  35887  prtlem18  35899  atlatmstc  36341  cvrexchlem  36441  paddasslem14  36855  pexmidlem5N  36996  cdleme29ex  37396  cdlemefr29exN  37424  cdleme32fva  37459  diarnN  38151  dihlsscpre  38256  isnacs3  39191  fnwe2lem2  39535  kelac1  39547  hbtlem5  39612  hbt  39614  dgraa0p  39633  monoordxrv  41642  rlimdmafv  43261  rlimdmafv2  43342  fmtnoprmfac2  43580  perfectALTVlem2  43738  mogoldbb  43801  mgmhmeql  43921  lindslinindsimp2  44420
  Copyright terms: Public domain W3C validator