Theorem simplrr 777

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 727	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5116  frpomin  6329  fsnex  7275  f1prex  7276  isotr  7328  weniso  7346  riota5f  7388  frxp2  8141  frxp3  8148  xpord3pred  8149  poseq  8155  fprlem2  8298  tfrlem9a  8398  oaass  8571  oeeui  8612  oaabs2  8659  coflton  8681  cofon1  8682  naddssim  8695  resixpfo  8948  omxpenlem  9085  pw2f1olem  9088  fopwdom  9092  fofinf1o  9342  marypha1lem  9443  ordiso2  9527  oismo  9552  ixpiunwdom  9602  cantnf  9705  ttrclss  9732  fseqenlem1  10036  iunfictbso  10126  dfac12lem2  10157  dfac12lem3  10158  infunsdom1  10224  infpssrlem5  10319  fin23lem24  10334  isf32lem2  10366  isf32lem4  10368  isf34lem4  10389  fin1a2lem12  10423  fin1a2lem13  10424  ttukeylem6  10526  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  winalim2  10708  wunex2  10750  tskord  10792  prlem934  11045  mulcmpblnr  11083  dedekind  11396  addrid  11413  cnegex  11414  negeu  11470  add20  11747  divdivdiv  11940  ltmul12a  12095  lemul12a  12097  lediv12a  12133  supaddc  12207  supmul1  12209  cru  12230  uzwo3  12957  xleadd1a  13267  xmullem  13278  xmulgt0  13297  xlemul1a  13302  ixxun  13376  ixxss12  13380  ioodisj  13497  fz0fzelfz0  13649  mulexpz  14118  rpexpmord  14184  leexp1a  14191  expmulnbnd  14251  hashf1  14473  fi1uzind  14523  brfi1indALT  14526  swrdccat  14751  reuccatpfxs1  14763  abs3lem  15355  rexanre  15363  cau3lem  15371  limsupgre  15495  limsupbnd2  15497  o1lo1  15551  rlimclim1  15559  rlimclim  15560  rlimcn1  15602  rlimcn3  15604  o1of2  15627  o1rlimmul  15633  lo1add  15641  lo1mul  15642  isercolllem1  15679  climcau  15685  caucvgrlem  15687  caucvgb  15694  summolem2  15730  summo  15731  modfsummod  15808  o1fsum  15827  prodmolem2  15949  addmodlteqALT  16342  rpdvds  16677  isprm5  16724  isprm6  16731  pclem  16856  pcqmul  16871  pcexp  16877  pcneg  16892  pcprmpw2  16900  pcadd  16907  pcmpt  16910  4sqlem13  16975  vdwlem2  17000  vdwlem7  17005  vdwlem12  17010  ramval  17026  ramub2  17032  ramz2  17042  ramcl  17047  cshwshashlem2  17114  imasval  17523  imasdsval  17527  mreexexd  17658  acsfn  17669  issubc3  17860  idfucl  17892  funcres2c  17914  isnat  17961  fucpropd  17991  xpcval  18187  xpcco  18193  prfval  18209  evlf2  18228  evlfcl  18232  curf12  18237  curf1cl  18238  curf2  18239  curfcl  18242  curf2ndf  18257  hof2val  18266  hofcl  18269  hofpropd  18277  yonedalem4a  18285  yonedainv  18291  drsdirfi  18315  pospo  18353  poslubmo  18419  posglbmo  18420  isipodrs  18545  acsinfd  18564  gsumvalx  18652  gsumpropd2lem  18655  mgmhmeql  18692  sgrppropd  18707  ismndd  18732  mndpropd  18735  mndpsuppss  18741  mhmeql  18802  mndind  18804  frmdup3lem  18842  mhmmnd  19045  issubg4  19126  ssnmz  19147  conjnmzb  19234  f1otrspeq  19426  psgneu  19485  pgpfi  19584  sylow2blem3  19601  slwhash  19603  fislw  19604  sylow3lem2  19607  lsmdisj2  19661  pj1eu  19675  efgredlem  19726  frgpuplem  19751  gexex  19832  frgpnabl  19854  dprdfadd  20001  dpjidcl  20039  pgpfac1lem3  20058  pgpfaclem3  20064  ablfac2  20070  ablsimpgcygd  20087  ablsimpgfind  20091  ablsimpgprmd  20096  rngpropd  20132  ringpropd  20246  imadrhmcl  20755  islmhm2  20994  lmhmpropd  21029  lbsextlem4  21120  prmirredlem  21431  psgndiflemA  21559  lsmcss  21650  uvcf1  21750  frlmsslsp  21754  frlmup1  21756  assapropd  21830  psrval  21873  evlslem1  22038  mamucl  22337  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  mamulid  22377  mamurid  22378  dmatsubcl  22434  dmatmulcl  22436  scmatscm  22449  marrepval  22498  marepveval  22504  mdetunilem7  22554  gsummatr01lem4  22594  cpmatmcllem  22654  mat2pmatf1  22665  mat2pmatlin  22671  decpmatmul  22708  pm2mpmhmlem2  22755  chpidmat  22783  pptbas  22944  toponmre  23029  restbas  23094  iscncl  23205  cnrest2  23222  cnpdis  23229  lmcnp  23240  dishaus  23318  cmpcovf  23327  tgcmp  23337  dfconn2  23355  clsconn  23366  2ndcctbss  23391  dis2ndc  23396  1stccnp  23398  islly2  23420  cldllycmp  23431  locfincmp  23462  comppfsc  23468  kgentopon  23474  txcls  23540  ptpjopn  23548  dfac14  23554  xkoccn  23555  txcnp  23556  txcmpb  23580  txlm  23584  xkopt  23591  xkoco1cn  23593  xkoco2cn  23594  qtopcn  23650  qtoprest  23653  regr1lem2  23676  xkocnv  23750  qtophmeo  23753  fmfnfmlem4  23893  hausflim  23917  hauspwpwf1  23923  fclscmp  23966  alexsublem  23980  alexsubALTlem2  23984  alexsubALTlem3  23985  ptcmplem3  23990  ptcmplem4  23991  ptcmplem5  23992  cnextfun  24000  tmdgsum2  24032  symgtgp  24042  tsmsval2  24066  tsmsgsum  24075  utoptop  24171  ismet2  24270  blin  24358  metss2lem  24448  methaus  24457  met1stc  24458  met2ndci  24459  prdsxmslem2  24466  metcnp3  24477  metcnpi3  24483  metustto  24490  metustfbas  24494  nlmvscn  24624  nrginvrcn  24629  xrsxmet  24747  reconnlem1  24764  reconn  24766  xrge0tsms  24772  xmetdcn2  24775  metdscn  24794  addcnlem  24802  fsumcn  24810  cnheiborlem  24902  cnheibor  24903  bndth  24906  lebnum  24912  nmoleub2lem2  25065  ipcn  25196  iscmet3  25243  caubl  25258  rrxdstprj1  25359  minveclem3b  25378  minveclem7  25385  pjthlem2  25388  pmltpc  25401  volfiniun  25498  ioombl1  25513  dyadss  25545  dyaddisjlem  25546  dyadmax  25549  dyadmbllem  25550  opnmbllem  25552  itg1addlem2  25648  itg10a  25661  mbfi1fseqlem6  25671  itg2seq  25693  itg2monolem1  25701  itg2gt0  25711  itgfsum  25778  limcfval  25823  ellimc2  25828  ellimc3  25830  limcres  25837  limciun  25845  dvres  25862  dveflem  25933  rolle  25944  dvlip2  25950  c1liplem1  25951  dvgt0lem1  25957  dvgt0  25959  dvlt0  25960  dvne0  25966  dvfsumrlimge0  25987  ftc1lem6  25998  itgsubst  26006  mdegmullem  26033  ply1domn  26079  ply1divex  26092  fta1g  26125  fta1b  26127  plyf  26153  dgrlem  26184  coeid  26193  plydivalg  26257  aannenlem1  26286  aalioulem3  26292  aalioulem6  26295  abelthlem8  26399  efif1olem4  26504  chordthm  26797  xrlimcnp  26928  jensen  26949  lgamcvglem  27000  lgamcvg2  27015  sqf11  27099  fsumvma2  27175  perfectlem2  27191  lgsdilem  27285  lgsquad2lem2  27346  lgsquad3  27348  2sqlem5  27383  2sqlem9  27388  2sqb  27393  rpvmasumlem  27448  dchrisum0flb  27471  dchrisum0  27481  pntpbnd  27549  pntibndlem3  27553  pntleml  27572  nolt02o  27657  nosupbday  27667  nosupbnd2  27678  noinfbday  27682  noinfbnd2  27693  noetasuplem4  27698  noetainflem4  27702  noetalem1  27703  conway  27761  slerec  27781  sltlpss  27862  addsprop  27926  remulscllem2  28350  tgjustc1  28400  tgjustc2  28401  legov  28510  legtrid  28516  tglinethru  28561  tglnpt2  28566  tglineintmo  28567  mirreu3  28579  perpcom  28638  colperpexlem3  28657  mideu  28663  opphllem1  28672  hlpasch  28681  lnopp2hpgb  28688  trgcopy  28729  brcgr  28825  brbtwn2  28830  colinearalg  28835  axsegcon  28852  axeuclidlem  28887  axcontlem9  28897  ecgrtg  28908  elntg  28909  eengtrkg  28911  upgr1eopALT  29042  usgredg4  29142  subuhgr  29211  subumgr  29213  usgr2wspthon  29893  clwlkclwwlkf1  29937  eupth2lems  30165  n4cyclfrgr  30218  vacn  30621  blocni  30732  ubthlem3  30799  minvecolem7  30810  chocunii  31228  pjhthmo  31229  pjhthlem2  31319  kbass5  32047  mdsymlem5  32334  foresf1o  32431  fcobij  32645  xrofsup  32690  mgcoval  32912  mgcf1o  32929  xrge0tsmsd  33002  symgcntz  33042  archirngz  33133  archiabllem2a  33138  isarchiofld  33285  prmidl2  33402  constrelextdg2  33727  smatrcl  33773  reff  33816  ordtconnlem1  33901  qqhval2  33959  volmeas  34208  fiunelcarsg  34294  ballotlemfc0  34471  ballotlemfcc  34472  signstfvneq0  34550  derangenlem  35139  erdsze2lem1  35171  pconnconn  35199  connpconn  35203  cvxsconn  35211  cvmliftmolem2  35250  cvmliftmo  35252  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  mrsubff1  35482  msubff1  35524  r1peuqusdeg1  35611  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeq  36094  ellines  36116  finminlem  36282  fnejoin2  36333  weiunso  36430  unbdqndv2  36475  irrdiff  37290  poimirlem13  37603  poimirlem14  37604  poimirlem32  37622  opnmbllem0  37626  mblfinlem3  37629  itg2addnclem  37641  itg2addnc  37644  ftc1cnnc  37662  upixp  37699  filbcmb  37710  sstotbnd2  37744  isbnd3  37754  prdsbnd2  37765  cntotbnd  37766  ismtyima  37773  bfp  37794  rrncmslem  37802  unichnidl  38001  lshpcmp  38952  islshpat  38981  lfl0f  39033  ishlat3N  39318  3dim1  39432  islvol5  39544  lvoli2  39546  lncvrelatN  39746  pclfinclN  39915  pexmidlem8N  39942  idltrn  40115  cdleme42keg  40451  cdleme42mgN  40453  cdlemf2  40527  cdlemg2cex  40556  trlcoat  40688  dihopelvalcpre  41213  dih1dimatlem  41294  dihjatcclem4  41386  lcfl7N  41466  lcfrlem9  41515  mapdh9a  41754  hdmapglem7  41894  aks4d1p8  42046  isprimroot  42052  evl1gprodd  42076  sticksstones11  42115  grpods  42153  aks5lem8  42160  renegeulemv  42358  sn-subeu  42416  remulinvcom  42422  sn-itrere  42458  sn-retire  42459  imacrhmcl  42484  fidomncyc  42505  fsuppind  42560  fsuppssind  42563  mhpind  42564  prjspertr  42575  prjspreln0  42579  flt4lem7  42629  nna4b4nsq  42630  nacsfix  42682  mzpsubst  42718  mzpcompact2lem  42721  eldioph2lem2  42731  eldioph2  42732  eldioph2b  42733  diophin  42742  diophun  42743  irrapxlem3  42794  irrapxlem5  42796  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrdich  42839  pell1qrge1  42840  pell1qrgaplem  42843  monotuz  42912  acongtr  42949  acongrep  42951  jm2.23  42967  jm2.26a  42971  jm2.26lem3  42972  jm2.26  42973  jm2.27  42979  wepwsolem  43013  fnwe2lem2  43022  kelac1  43034  kercvrlsm  43054  hbtlem5  43099  hbt  43101  mpaaeu  43121  cantnfresb  43295  onmcl  43302  tfsconcatun  43308  tfsconcatfn  43309  tfsconcatfv1  43310  tfsconcatfv2  43311  naddcnff  43333  rfovcnvf1od  43975  mnurndlem1  44253  cncmpmax  45004  rfcnnnub  45008  disjxp1  45041  iccintsng  45500  fprodcn  45577  lptioo2  45608  lptioo1  45609  limclner  45628  stoweidlem31  46008  stoweidlem34  46011  stoweidlem35  46012  stoweidlem49  46026  stoweidlem59  46036  stoweidlem62  46039  fourierdlem60  46143  fourierdlem61  46144  fourierdlem87  46170  iundjiun  46437  ismeannd  46444  hoidmvle  46577  smfsuplem2  46789  2reu8i  47090  prproropf1olem2  47466  paireqne  47473  perfectALTVlem2  47684  mogoldbb  47747  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  grimedg  47896  scmsuppss  48294  lindslinindsimp2lem5  48386  elfzolborelfzop1  48443  elbigolo1  48485  itschlc0xyqsol1  48694  itschlc0xyqsol  48695  iccdisj  48820  toslat  48904  iinfssclem3  48971  iinfssc  48972  iinfsubc  48973  imasubc3  49044  upciclem4  49052  tposcurf1  49158  fuco22  49198  fuco22natlem  49204  functhinclem4  49281  arweuthinc  49362