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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 471 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 760 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  f1prex  6416  grpridd  6749  wfrlem17  7295  eroveu  7706  undom  7910  mapdom2  7993  domunfican  8095  fofinf1o  8103  finsschain  8133  wemaplem3  8313  oemapvali  8441  iunfictbso  8797  enfin2i  9003  fin1a2s  9096  ttukeylem6  9196  distrlem4pr  9704  mulcmpblnr  9748  prsrlem1  9749  dedekind  10051  divdivdiv  10577  divmuleq  10581  divsubdiv  10592  lediv12a  10767  xralrple  11871  ssfzo12bi  12386  seqcaopr  12657  leexp2r  12737  hashbclem  13047  wrd2ind  13277  rtrclreclem3  13596  rtrclreclem4  13597  relexpindlem  13599  rtrclind  13601  rlimresb  14092  summo  14243  fsum2dlem  14291  prodmo  14453  fprod2dlem  14497  bezoutlem3  15044  bezoutlem4  15045  ncoprmgcdne1b  15149  qredeu  15158  coprmproddvdslem  15162  pcqmul  15344  pcadd  15379  pockthg  15396  prmreclem2  15407  vdwlem10  15480  ramub1lem2  15517  prmgaplem6  15546  prmgaplem7  15547  cshwsdisj  15591  mreexexlem4d  16078  mreexdomd  16081  issubc3  16280  cofucl  16319  setcmon  16508  setcepi  16509  drsdirfi  16709  poslubmo  16917  posglbmo  16918  issubmd  17120  mrcmndind  17137  ghmpreima  17453  gaorber  17512  psgnunilem4  17688  psgneu  17697  odcau  17790  pgpssslw  17800  fislw  17811  lsmsubm  17839  efgsfo  17923  gsum2d2  18144  pgpfac1lem5  18249  pgpfac1  18250  pgpfaclem2  18252  pgpfaclem3  18253  unitgrp  18438  lmodprop2d  18696  lsspropd  18786  lbsextlem4  18930  assapropd  19096  evlslem1  19284  mdetunilem8  20191  mdetuni0  20193  mdetmul  20195  neiint  20665  restbas  20719  iscnp4  20824  cnpco  20828  nrmsep  20918  regsep2  20937  ordthauslem  20944  1stcfb  21005  1stcrest  21013  2ndcctbss  21015  2ndcdisj  21016  2ndcomap  21018  dis2ndc  21020  nlly2i  21036  islly2  21044  hausllycmp  21054  lly1stc  21056  comppfsc  21092  ptbasin  21137  txcls  21164  ptcnp  21182  txlly  21196  txnlly  21197  txtube  21200  txcmplem1  21201  txcmplem2  21202  xkococnlem  21219  basqtop  21271  regr1lem  21299  kqreglem1  21301  kqreglem2  21302  kqnrmlem1  21303  kqnrmlem2  21304  reghmph  21353  nrmhmph  21354  opnfbas  21403  rnelfmlem  21513  fmufil  21520  fclscf  21586  fclsfnflim  21588  flimfnfcls  21589  uffclsflim  21592  cnpfcfi  21601  cnpfcf  21602  alexsubALTlem2  21609  alexsubALTlem4  21611  tgpconcompeqg  21672  ghmcnp  21675  qustgplem  21681  tsmsxp  21715  blssps  21986  blss  21987  blcld  22067  metequiv2  22072  met2ndci  22084  prdsxmslem2  22091  txmetcnp  22109  nlmvscnlem1  22247  xrge0tsms  22392  ipcnlem1  22796  iscmet3  22843  cmetss  22865  minveclem3  22952  pmltpc  22970  ovolscalem2  23033  ovolicc2lem5  23040  ovolicc2  23041  nulmbl2  23055  ioombl1  23081  uniioombllem6  23106  uniioombl  23107  vitalilem3  23129  i1faddlem  23210  mbfmullem  23242  itg2split  23266  lhop2  23526  dvfsumrlim  23542  itgsubst  23560  plydivex  23800  plyexmo  23816  ulmbdd  23900  cxploglim  24448  dchrptlem2  24734  lgsquad2lem2  24854  2sqlem5  24891  dchrvmasumif  24936  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lem3  24952  dchrisum0  24953  dchrmusum  24957  dchrvmasum  24958  pntibndlem3  25025  pntlemp  25043  ostth3  25071  legtrid  25231  hlcgreu  25258  mirreu3  25294  midexlem  25332  opphllem  25372  mideulem  25373  opphllem1  25384  oppperpex  25390  lnperpex  25440  trgcopy  25441  iscgra1  25447  cgraswap  25457  cgracom  25459  cgratr  25460  acopyeu  25470  ax5seglem9  25562  ax5seg  25563  axcontlem8  25596  axcontlem12  25600  cusgrafilem1  25800  2spotiundisj  26382  ablo4  26581  smcnlem  26729  pjhthmo  27338  mdslmd1lem1  28361  xrge0tsmsd  28909  locfinref  29029  xpinpreima2  29074  qqhval2  29147  dya2iocnrect  29463  orvcgteel  29649  orvclteel  29654  derangenlem  30200  cnpcon  30259  txpcon  30261  conpcon  30264  pconpi1  30266  iccllyscon  30279  rellyscon  30280  cvmcov2  30304  cvmliftmolem2  30311  cvmliftmo  30313  cvmliftlem15  30327  cvmliftpht  30347  cvmlift3lem2  30349  cgrextend  31078  btwnouttr2  31092  cgrsub  31115  cgrxfr  31125  btwnxfr  31126  colineardim1  31131  btwnconn1lem6  31162  btwnconn1lem13  31169  btwnconn1lem14  31170  btwnconn3  31173  seglecgr12im  31180  segleantisym  31185  outsideofeq  31200  outsidele  31202  lineunray  31217  linethru  31223  fnessref  31315  neibastop2lem  31318  neibastop2  31319  unblimceq0lem  31460  knoppndvlem22  31487  bj-finsumval0  32107  isbasisrelowllem1  32162  isbasisrelowllem2  32163  mblfinlem3  32401  cnambfre  32411  areacirclem5  32457  istotbnd3  32523  sstotbnd  32527  crngm4  32755  cvlcvr1  33427  4atlem12  33699  paddasslem10  33916  paddasslem12  33918  paddasslem13  33919  lhpexle3lem  34098  cdlemd4  34289  cdleme0cq  34303  cdlemefs32sn1aw  34503  cdleme43fsv1snlem  34509  cdleme32d  34533  cdleme32f  34535  cdleme40m  34556  cdleme40n  34557  cdleme42keg  34575  cdleme42mgN  34577  cdleme50trn2  34640  cdleme50trn3  34642  cdlemm10N  35208  dihvalcqpre  35325  dihopelvalcpre  35338  dihmeetlem1N  35380  dihjat1lem  35518  mapd0  35755  mapdh9a  35880  diophin  36137  pellexlem3  36196  pellexlem5  36198  pellex  36200  pell14qrmulcl  36228  jm2.19lem3  36359  jm2.25  36367  jm2.27b  36374  lmhmfgsplit  36457  hbtlem2  36496  hbtlem5  36500  gsumws3  37304  gsumws4  37305  fnchoice  37994  stoweidlem17  38693  stoweidlem53  38729  stoweidlem61  38737  qndenserrnbllem  38973  bgoldbtbnd  40009  2pthfrgr  41435  frgrnbnb  41444  rabsubmgmd  41562  lindslinindsimp1  42021
  Copyright terms: Public domain W3C validator