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

Theorem simplrr 774
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrr (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 485 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 723 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:  disjxiun  5055  fsnex  7030  f1prex  7031  isotr  7078  weniso  7096  riota5f  7131  tfrlem9a  8013  oaass  8177  oeeui  8218  oaabs2  8262  resixpfo  8489  omxpenlem  8607  pw2f1olem  8610  fopwdom  8614  fofinf1o  8788  marypha1lem  8886  ordiso2  8968  oismo  8993  ixpiunwdom  9044  cantnf  9145  fseqenlem1  9439  iunfictbso  9529  dfac12lem2  9559  dfac12lem3  9560  infunsdom1  9624  infpssrlem5  9718  fin23lem24  9733  isf32lem2  9765  isf32lem4  9767  isf34lem4  9788  fin1a2lem12  9822  fin1a2lem13  9823  ttukeylem6  9925  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  winalim2  10107  wunex2  10149  tskord  10191  prlem934  10444  mulcmpblnr  10482  dedekind  10792  addid1  10809  cnegex  10810  negeu  10865  add20  11141  divdivdiv  11330  ltmul12a  11485  lemul12a  11487  lediv12a  11522  supaddc  11597  supmul1  11599  cru  11619  uzwo3  12332  xleadd1a  12636  xmullem  12647  xmulgt0  12666  xlemul1a  12671  ixxun  12744  ixxss12  12748  ioodisj  12858  fz0fzelfz0  13003  mulexpz  13459  rpexpmord  13522  leexp1a  13529  expmulnbnd  13586  hashf1  13805  fi1uzind  13845  brfi1indALT  13848  swrdccat  14087  reuccatpfxs1  14099  abs3lem  14688  rexanre  14696  cau3lem  14704  limsupgre  14828  limsupbnd2  14830  o1lo1  14884  rlimclim1  14892  rlimclim  14893  rlimcn1  14935  rlimcn2  14937  o1of2  14959  o1rlimmul  14965  lo1add  14973  lo1mul  14974  isercolllem1  15011  climcau  15017  caucvgrlem  15019  caucvgb  15026  summolem2  15063  summo  15064  modfsummod  15139  o1fsum  15158  prodmolem2  15279  addmodlteqALT  15665  rpdvds  15994  isprm5  16041  isprm6  16048  pclem  16165  pcqmul  16180  pcexp  16186  pcneg  16200  pcprmpw2  16208  pcadd  16215  pcmpt  16218  4sqlem13  16283  vdwlem2  16308  vdwlem7  16313  vdwlem12  16318  ramval  16334  ramub2  16340  ramz2  16350  ramcl  16355  cshwshashlem2  16420  imasval  16774  imasdsval  16778  mreexexd  16909  acsfn  16920  issubc3  17109  idfucl  17141  funcres2c  17161  isnat  17207  fucpropd  17237  xpcval  17417  xpcco  17423  prfval  17439  evlf2  17458  evlfcl  17462  curf12  17467  curf1cl  17468  curf2  17469  curfcl  17472  curf2ndf  17487  hof2val  17496  hofcl  17499  hofpropd  17507  yonedalem4a  17515  yonedainv  17521  drsdirfi  17538  pospo  17573  poslubmo  17746  posglbmo  17747  isipodrs  17761  acsinfd  17780  gsumvalx  17876  gsumpropd2lem  17879  ismndd  17923  mndpropd  17926  mhmeql  17980  mndind  17982  frmdup3lem  18021  mhmmnd  18161  issubg4  18238  ssnmz  18258  conjnmzb  18333  f1otrspeq  18506  psgneu  18565  pgpfi  18661  sylow2blem3  18678  slwhash  18680  fislw  18681  sylow3lem2  18684  lsmdisj2  18739  pj1eu  18753  efgredlem  18804  frgpuplem  18829  gexex  18904  frgpnabl  18926  dprdfadd  19073  dpjidcl  19111  pgpfac1lem3  19130  pgpfaclem3  19136  ablfac2  19142  ablsimpgcygd  19159  ablsimpgfind  19163  ablsimpgprmd  19168  ringpropd  19263  islmhm2  19741  lmhmpropd  19776  lbsextlem4  19864  assapropd  20031  psrval  20072  evlslem1  20225  prmirredlem  20570  psgndiflemA  20675  lsmcss  20766  uvcf1  20866  frlmsslsp  20870  frlmup1  20872  mamucl  20940  mamuass  20941  mamudi  20942  mamudir  20943  mamuvs1  20944  mamuvs2  20945  mamulid  20980  mamurid  20981  dmatsubcl  21037  dmatmulcl  21039  scmatscm  21052  marrepval  21101  marepveval  21107  mdetunilem7  21157  gsummatr01lem4  21197  cpmatmcllem  21256  mat2pmatf1  21267  mat2pmatlin  21273  decpmatmul  21310  pm2mpmhmlem2  21357  chpidmat  21385  pptbas  21546  toponmre  21631  restbas  21696  iscncl  21807  cnrest2  21824  cnpdis  21831  lmcnp  21842  dishaus  21920  cmpcovf  21929  tgcmp  21939  dfconn2  21957  clsconn  21968  2ndcctbss  21993  dis2ndc  21998  1stccnp  22000  islly2  22022  cldllycmp  22033  locfincmp  22064  comppfsc  22070  kgentopon  22076  txcls  22142  ptpjopn  22150  dfac14  22156  xkoccn  22157  txcnp  22158  txcmpb  22182  txlm  22186  xkopt  22193  xkoco1cn  22195  xkoco2cn  22196  qtopcn  22252  qtoprest  22255  regr1lem2  22278  xkocnv  22352  qtophmeo  22355  fmfnfmlem4  22495  hausflim  22519  hauspwpwf1  22525  fclscmp  22568  alexsublem  22582  alexsubALTlem2  22586  alexsubALTlem3  22587  ptcmplem3  22592  ptcmplem4  22593  ptcmplem5  22594  cnextfun  22602  tmdgsum2  22634  symgtgp  22639  tsmsval2  22667  tsmsgsum  22676  utoptop  22772  ismet2  22872  blin  22960  metss2lem  23050  methaus  23059  met1stc  23060  met2ndci  23061  prdsxmslem2  23068  metcnp3  23079  metcnpi3  23085  metustto  23092  metustfbas  23096  nlmvscn  23225  nrginvrcn  23230  xrsxmet  23346  reconnlem1  23363  reconn  23365  xrge0tsms  23371  xmetdcn2  23374  metdscn  23393  addcnlem  23401  fsumcn  23407  cnheiborlem  23487  cnheibor  23488  bndth  23491  lebnum  23497  nmoleub2lem2  23649  ipcn  23778  iscmet3  23825  caubl  23840  rrxdstprj1  23941  minveclem3b  23960  minveclem7  23967  pjthlem2  23970  pmltpc  23980  volfiniun  24077  ioombl1  24092  dyadss  24124  dyaddisjlem  24125  dyadmax  24128  dyadmbllem  24129  opnmbllem  24131  itg1addlem2  24227  itg10a  24240  mbfi1fseqlem6  24250  itg2seq  24272  itg2monolem1  24280  itg2gt0  24290  itgfsum  24356  limcfval  24399  ellimc2  24404  ellimc3  24406  limcres  24413  limciun  24421  dvres  24438  dveflem  24505  rolle  24516  dvlip2  24521  c1liplem1  24522  dvgt0lem1  24528  dvgt0  24530  dvlt0  24531  dvne0  24537  dvfsumrlimge0  24556  ftc1lem6  24567  itgsubst  24575  mdegmullem  24601  ply1domn  24646  ply1divex  24659  fta1g  24690  fta1b  24692  plyf  24717  dgrlem  24748  coeid  24757  plydivalg  24817  aannenlem1  24846  aalioulem3  24852  aalioulem6  24855  abelthlem8  24956  efif1olem4  25056  chordthm  25342  xrlimcnp  25474  jensen  25494  lgamcvglem  25545  lgamcvg2  25560  sqf11  25644  fsumvma2  25718  perfectlem2  25734  lgsdilem  25828  lgsquad2lem2  25889  lgsquad3  25891  2sqlem5  25926  2sqlem9  25931  2sqb  25936  rpvmasumlem  25991  dchrisum0flb  26014  dchrisum0  26024  pntpbnd  26092  pntibndlem3  26096  pntleml  26115  tgjustc1  26189  tgjustc2  26190  legov  26299  legtrid  26305  tglinethru  26350  tglnpt2  26355  tglineintmo  26356  mirreu3  26368  perpcom  26427  colperpexlem3  26446  mideu  26452  opphllem1  26461  hlpasch  26470  lnopp2hpgb  26477  trgcopy  26518  brcgr  26614  brbtwn2  26619  colinearalg  26624  axsegcon  26641  axeuclidlem  26676  axcontlem9  26686  ecgrtg  26697  elntg  26698  eengtrkg  26700  upgr1eopALT  26830  usgredg4  26927  subuhgr  26996  subumgr  26998  usgr2wspthon  27672  clwlkclwwlkf1  27716  eupth2lems  27945  n4cyclfrgr  27998  vacn  28399  blocni  28510  ubthlem3  28577  minvecolem7  28588  chocunii  29006  pjhthmo  29007  pjhthlem2  29097  kbass5  29825  mdsymlem5  30112  foresf1o  30193  fcobij  30385  xrofsup  30419  xrge0tsmsd  30620  symgcntz  30657  archirngz  30746  archiabllem2a  30751  isarchiofld  30818  prmidl2  30878  smatrcl  30961  reff  31003  ordtconnlem1  31067  qqhval2  31123  volmeas  31390  fiunelcarsg  31474  ballotlemfc0  31650  ballotlemfcc  31651  signstfvneq0  31742  derangenlem  32316  erdsze2lem1  32348  pconnconn  32376  connpconn  32380  cvxsconn  32388  cvmliftmolem2  32427  cvmliftmo  32429  cvmlift2lem10  32457  cvmlift2lem12  32459  cvmlift3lem7  32470  mrsubff1  32659  msubff1  32701  frpomin  32976  poseq  32993  fprlem2  33036  nolt02o  33097  noprefixmo  33100  nosupbnd2  33114  noetalem3  33117  noetalem5  33119  conway  33162  slerec  33175  ifscgr  33403  cgrxfr  33414  btwnconn1lem13  33458  btwnconn1lem14  33459  outsideofeq  33489  ellines  33511  finminlem  33564  fnejoin2  33615  unbdqndv2  33748  poimirlem13  34787  poimirlem14  34788  poimirlem32  34806  opnmbllem0  34810  mblfinlem3  34813  itg2addnclem  34825  itg2addnc  34828  ftc1cnnc  34848  upixp  34887  filbcmb  34898  sstotbnd2  34935  isbnd3  34945  prdsbnd2  34956  cntotbnd  34957  ismtyima  34964  bfp  34985  rrncmslem  34993  unichnidl  35192  lshpcmp  36006  islshpat  36035  lfl0f  36087  ishlat3N  36372  3dim1  36485  islvol5  36597  lvoli2  36599  lncvrelatN  36799  pclfinclN  36968  pexmidlem8N  36995  idltrn  37168  cdleme42keg  37504  cdleme42mgN  37506  cdlemf2  37580  cdlemg2cex  37609  trlcoat  37741  dihopelvalcpre  38266  dih1dimatlem  38347  dihjatcclem4  38439  lcfl7N  38519  lcfrlem9  38568  mapdh9a  38807  hdmapglem7  38947  renegeulemv  39078  remulinvcom  39128  prjspertr  39135  prjspreln0  39139  nacsfix  39189  mzpsubst  39225  mzpcompact2lem  39228  eldioph2lem2  39238  eldioph2  39239  eldioph2b  39240  diophin  39249  diophun  39250  irrapxlem3  39301  irrapxlem5  39303  pell1234qrreccl  39331  pell1234qrmulcl  39332  pell14qrdich  39346  pell1qrge1  39347  pell1qrgaplem  39350  monotuz  39418  acongtr  39455  acongrep  39457  jm2.23  39473  jm2.26a  39477  jm2.26lem3  39478  jm2.26  39479  jm2.27  39485  wepwsolem  39522  fnwe2lem2  39531  kelac1  39543  kercvrlsm  39563  hbtlem5  39608  hbt  39610  mpaaeu  39630  rfovcnvf1od  40230  mnurndlem1  40497  cncmpmax  41169  rfcnnnub  41173  disjxp1  41211  iccintsng  41679  fprodcn  41761  lptioo2  41792  lptioo1  41793  limclner  41812  stoweidlem31  42197  stoweidlem34  42200  stoweidlem35  42201  stoweidlem49  42215  stoweidlem59  42225  stoweidlem62  42228  fourierdlem60  42332  fourierdlem61  42333  fourierdlem87  42359  iundjiun  42623  ismeannd  42630  hoidmvle  42763  smfsuplem2  42967  2reu8i  43193  prproropf1olem2  43513  paireqne  43520  perfectALTVlem2  43734  mogoldbb  43797  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  isomgrtrlem  43850  mgmhmeql  43917  mndpsuppss  44317  scmsuppss  44318  lindslinindsimp2lem5  44415  elfzolborelfzop1  44472  elbigolo1  44515  itschlc0xyqsol1  44651  itschlc0xyqsol  44652
  Copyright terms: Public domain W3C validator