Theorem simplrr 775

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 485	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 724	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

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 206  df-an 397

This theorem is referenced by:  disjxiun  5072  frpomin  6247  fsnex  7164  f1prex  7165  isotr  7216  weniso  7234  riota5f  7270  fprlem2  8126  tfrlem9a  8226  oaass  8401  oeeui  8442  oaabs2  8488  resixpfo  8733  omxpenlem  8869  pw2f1olem  8872  fopwdom  8876  fofinf1o  9103  marypha1lem  9201  ordiso2  9283  oismo  9308  ixpiunwdom  9358  cantnf  9460  ttrclss  9487  fseqenlem1  9789  iunfictbso  9879  dfac12lem2  9909  dfac12lem3  9910  infunsdom1  9978  infpssrlem5  10072  fin23lem24  10087  isf32lem2  10119  isf32lem4  10121  isf34lem4  10142  fin1a2lem12  10176  fin1a2lem13  10177  ttukeylem6  10279  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  winalim2  10461  wunex2  10503  tskord  10545  prlem934  10798  mulcmpblnr  10836  dedekind  11147  addid1  11164  cnegex  11165  negeu  11220  add20  11496  divdivdiv  11685  ltmul12a  11840  lemul12a  11842  lediv12a  11877  supaddc  11951  supmul1  11953  cru  11974  uzwo3  12692  xleadd1a  12996  xmullem  13007  xmulgt0  13026  xlemul1a  13031  ixxun  13104  ixxss12  13108  ioodisj  13223  fz0fzelfz0  13371  mulexpz  13832  rpexpmord  13895  leexp1a  13902  expmulnbnd  13959  hashf1  14180  fi1uzind  14220  brfi1indALT  14223  swrdccat  14457  reuccatpfxs1  14469  abs3lem  15059  rexanre  15067  cau3lem  15075  limsupgre  15199  limsupbnd2  15201  o1lo1  15255  rlimclim1  15263  rlimclim  15264  rlimcn1  15306  rlimcn3  15308  o1of2  15331  o1rlimmul  15337  lo1add  15345  lo1mul  15346  isercolllem1  15385  climcau  15391  caucvgrlem  15393  caucvgb  15400  summolem2  15437  summo  15438  modfsummod  15515  o1fsum  15534  prodmolem2  15654  addmodlteqALT  16043  rpdvds  16374  isprm5  16421  isprm6  16428  pclem  16548  pcqmul  16563  pcexp  16569  pcneg  16584  pcprmpw2  16592  pcadd  16599  pcmpt  16602  4sqlem13  16667  vdwlem2  16692  vdwlem7  16697  vdwlem12  16702  ramval  16718  ramub2  16724  ramz2  16734  ramcl  16739  cshwshashlem2  16807  imasval  17231  imasdsval  17235  mreexexd  17366  acsfn  17377  issubc3  17573  idfucl  17605  funcres2c  17626  isnat  17672  fucpropd  17704  xpcval  17903  xpcco  17909  prfval  17925  evlf2  17945  evlfcl  17949  curf12  17954  curf1cl  17955  curf2  17956  curfcl  17959  curf2ndf  17974  hof2val  17983  hofcl  17986  hofpropd  17994  yonedalem4a  18002  yonedainv  18008  drsdirfi  18032  pospo  18072  poslubmo  18138  posglbmo  18139  isipodrs  18264  acsinfd  18283  gsumvalx  18369  gsumpropd2lem  18372  ismndd  18416  mndpropd  18419  mhmeql  18473  mndind  18475  frmdup3lem  18514  mhmmnd  18706  issubg4  18783  ssnmz  18803  conjnmzb  18878  f1otrspeq  19064  psgneu  19123  pgpfi  19219  sylow2blem3  19236  slwhash  19238  fislw  19239  sylow3lem2  19242  lsmdisj2  19297  pj1eu  19311  efgredlem  19362  frgpuplem  19387  gexex  19463  frgpnabl  19485  dprdfadd  19632  dpjidcl  19670  pgpfac1lem3  19689  pgpfaclem3  19695  ablfac2  19701  ablsimpgcygd  19718  ablsimpgfind  19722  ablsimpgprmd  19727  ringpropd  19830  islmhm2  20309  lmhmpropd  20344  lbsextlem4  20432  prmirredlem  20703  psgndiflemA  20815  lsmcss  20906  uvcf1  21008  frlmsslsp  21012  frlmup1  21014  assapropd  21085  psrval  21127  evlslem1  21301  mamucl  21557  mamuass  21558  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  mamulid  21599  mamurid  21600  dmatsubcl  21656  dmatmulcl  21658  scmatscm  21671  marrepval  21720  marepveval  21726  mdetunilem7  21776  gsummatr01lem4  21816  cpmatmcllem  21876  mat2pmatf1  21887  mat2pmatlin  21893  decpmatmul  21930  pm2mpmhmlem2  21977  chpidmat  22005  pptbas  22167  toponmre  22253  restbas  22318  iscncl  22429  cnrest2  22446  cnpdis  22453  lmcnp  22464  dishaus  22542  cmpcovf  22551  tgcmp  22561  dfconn2  22579  clsconn  22590  2ndcctbss  22615  dis2ndc  22620  1stccnp  22622  islly2  22644  cldllycmp  22655  locfincmp  22686  comppfsc  22692  kgentopon  22698  txcls  22764  ptpjopn  22772  dfac14  22778  xkoccn  22779  txcnp  22780  txcmpb  22804  txlm  22808  xkopt  22815  xkoco1cn  22817  xkoco2cn  22818  qtopcn  22874  qtoprest  22877  regr1lem2  22900  xkocnv  22974  qtophmeo  22977  fmfnfmlem4  23117  hausflim  23141  hauspwpwf1  23147  fclscmp  23190  alexsublem  23204  alexsubALTlem2  23208  alexsubALTlem3  23209  ptcmplem3  23214  ptcmplem4  23215  ptcmplem5  23216  cnextfun  23224  tmdgsum2  23256  symgtgp  23266  tsmsval2  23290  tsmsgsum  23299  utoptop  23395  ismet2  23495  blin  23583  metss2lem  23676  methaus  23685  met1stc  23686  met2ndci  23687  prdsxmslem2  23694  metcnp3  23705  metcnpi3  23711  metustto  23718  metustfbas  23722  nlmvscn  23860  nrginvrcn  23865  xrsxmet  23981  reconnlem1  23998  reconn  24000  xrge0tsms  24006  xmetdcn2  24009  metdscn  24028  addcnlem  24036  fsumcn  24042  cnheiborlem  24126  cnheibor  24127  bndth  24130  lebnum  24136  nmoleub2lem2  24288  ipcn  24419  iscmet3  24466  caubl  24481  rrxdstprj1  24582  minveclem3b  24601  minveclem7  24608  pjthlem2  24611  pmltpc  24623  volfiniun  24720  ioombl1  24735  dyadss  24767  dyaddisjlem  24768  dyadmax  24771  dyadmbllem  24772  opnmbllem  24774  itg1addlem2  24870  itg10a  24884  mbfi1fseqlem6  24894  itg2seq  24916  itg2monolem1  24924  itg2gt0  24934  itgfsum  25000  limcfval  25045  ellimc2  25050  ellimc3  25052  limcres  25059  limciun  25067  dvres  25084  dveflem  25152  rolle  25163  dvlip2  25168  c1liplem1  25169  dvgt0lem1  25175  dvgt0  25177  dvlt0  25178  dvne0  25184  dvfsumrlimge0  25203  ftc1lem6  25214  itgsubst  25222  mdegmullem  25252  ply1domn  25297  ply1divex  25310  fta1g  25341  fta1b  25343  plyf  25368  dgrlem  25399  coeid  25408  plydivalg  25468  aannenlem1  25497  aalioulem3  25503  aalioulem6  25506  abelthlem8  25607  efif1olem4  25710  chordthm  25996  xrlimcnp  26127  jensen  26147  lgamcvglem  26198  lgamcvg2  26213  sqf11  26297  fsumvma2  26371  perfectlem2  26387  lgsdilem  26481  lgsquad2lem2  26542  lgsquad3  26544  2sqlem5  26579  2sqlem9  26584  2sqb  26589  rpvmasumlem  26644  dchrisum0flb  26667  dchrisum0  26677  pntpbnd  26745  pntibndlem3  26749  pntleml  26768  tgjustc1  26845  tgjustc2  26846  legov  26955  legtrid  26961  tglinethru  27006  tglnpt2  27011  tglineintmo  27012  mirreu3  27024  perpcom  27083  colperpexlem3  27102  mideu  27108  opphllem1  27117  hlpasch  27126  lnopp2hpgb  27133  trgcopy  27174  brcgr  27277  brbtwn2  27282  colinearalg  27287  axsegcon  27304  axeuclidlem  27339  axcontlem9  27349  ecgrtg  27360  elntg  27361  eengtrkg  27363  upgr1eopALT  27496  usgredg4  27593  subuhgr  27662  subumgr  27664  usgr2wspthon  28339  clwlkclwwlkf1  28383  eupth2lems  28611  n4cyclfrgr  28664  vacn  29065  blocni  29176  ubthlem3  29243  minvecolem7  29254  chocunii  29672  pjhthmo  29673  pjhthlem2  29763  kbass5  30491  mdsymlem5  30778  foresf1o  30859  fcobij  31066  xrofsup  31099  mgcoval  31273  mgcf1o  31290  xrge0tsmsd  31326  symgcntz  31363  archirngz  31452  archiabllem2a  31457  isarchiofld  31525  prmidl2  31625  smatrcl  31755  reff  31798  ordtconnlem1  31883  qqhval2  31941  volmeas  32208  fiunelcarsg  32292  ballotlemfc0  32468  ballotlemfcc  32469  signstfvneq0  32560  derangenlem  33142  erdsze2lem1  33174  pconnconn  33202  connpconn  33206  cvxsconn  33214  cvmliftmolem2  33253  cvmliftmo  33255  cvmlift2lem10  33283  cvmlift2lem12  33285  cvmlift3lem7  33296  mrsubff1  33485  msubff1  33527  frxp2  33800  frxp3  33806  poseq  33811  naddssim  33846  nolt02o  33907  nosupbday  33917  nosupbnd2  33928  noinfbday  33932  noinfbnd2  33943  noetasuplem4  33948  noetainflem4  33952  noetalem1  33953  conway  34002  slerec  34022  sltlpss  34096  ifscgr  34355  cgrxfr  34366  btwnconn1lem13  34410  btwnconn1lem14  34411  outsideofeq  34441  ellines  34463  finminlem  34516  fnejoin2  34567  unbdqndv2  34700  irrdiff  35506  poimirlem13  35799  poimirlem14  35800  poimirlem32  35818  opnmbllem0  35822  mblfinlem3  35825  itg2addnclem  35837  itg2addnc  35840  ftc1cnnc  35858  upixp  35896  filbcmb  35907  sstotbnd2  35941  isbnd3  35951  prdsbnd2  35962  cntotbnd  35963  ismtyima  35970  bfp  35991  rrncmslem  35999  unichnidl  36198  lshpcmp  37009  islshpat  37038  lfl0f  37090  ishlat3N  37375  3dim1  37488  islvol5  37600  lvoli2  37602  lncvrelatN  37802  pclfinclN  37971  pexmidlem8N  37998  idltrn  38171  cdleme42keg  38507  cdleme42mgN  38509  cdlemf2  38583  cdlemg2cex  38612  trlcoat  38744  dihopelvalcpre  39269  dih1dimatlem  39350  dihjatcclem4  39442  lcfl7N  39522  lcfrlem9  39571  mapdh9a  39810  hdmapglem7  39950  aks4d1p8  40102  sticksstones11  40119  fsuppind  40286  fsuppssind  40289  mhpind  40290  mhphf  40292  renegeulemv  40358  sn-subeu  40415  remulinvcom  40421  itrere  40443  retire  40444  prjspertr  40451  prjspreln0  40455  flt4lem7  40503  nna4b4nsq  40504  nacsfix  40541  mzpsubst  40577  mzpcompact2lem  40580  eldioph2lem2  40590  eldioph2  40591  eldioph2b  40592  diophin  40601  diophun  40602  irrapxlem3  40653  irrapxlem5  40655  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell14qrdich  40698  pell1qrge1  40699  pell1qrgaplem  40702  monotuz  40770  acongtr  40807  acongrep  40809  jm2.23  40825  jm2.26a  40829  jm2.26lem3  40830  jm2.26  40831  jm2.27  40837  wepwsolem  40874  fnwe2lem2  40883  kelac1  40895  kercvrlsm  40915  hbtlem5  40960  hbt  40962  mpaaeu  40982  rfovcnvf1od  41619  mnurndlem1  41906  cncmpmax  42582  rfcnnnub  42586  disjxp1  42624  iccintsng  43068  fprodcn  43148  lptioo2  43179  lptioo1  43180  limclner  43199  stoweidlem31  43579  stoweidlem34  43582  stoweidlem35  43583  stoweidlem49  43597  stoweidlem59  43607  stoweidlem62  43610  fourierdlem60  43714  fourierdlem61  43715  fourierdlem87  43741  iundjiun  44005  ismeannd  44012  hoidmvle  44145  smfsuplem2  44356  2reu8i  44616  prproropf1olem2  44967  paireqne  44974  perfectALTVlem2  45185  mogoldbb  45248  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  isomgrtrlem  45301  mgmhmeql  45368  mndpsuppss  45718  scmsuppss  45719  lindslinindsimp2lem5  45814  elfzolborelfzop1  45871  elbigolo1  45914  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  iccdisj  46203  toslat  46279  functhinclem4  46336