Theorem simplrr 776

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 725	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  5107  frpomin  6299  fsnex  7234  f1prex  7235  isotr  7286  weniso  7304  riota5f  7347  frxp2  8081  frxp3  8088  xpord3pred  8089  poseq  8095  fprlem2  8237  tfrlem9a  8337  oaass  8513  oeeui  8554  oaabs2  8600  coflton  8622  cofon1  8623  naddssim  8636  resixpfo  8881  omxpenlem  9024  pw2f1olem  9027  fopwdom  9031  fofinf1o  9278  marypha1lem  9378  ordiso2  9460  oismo  9485  ixpiunwdom  9535  cantnf  9638  ttrclss  9665  fseqenlem1  9969  iunfictbso  10059  dfac12lem2  10089  dfac12lem3  10090  infunsdom1  10158  infpssrlem5  10252  fin23lem24  10267  isf32lem2  10299  isf32lem4  10301  isf34lem4  10322  fin1a2lem12  10356  fin1a2lem13  10357  ttukeylem6  10459  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  winalim2  10641  wunex2  10683  tskord  10725  prlem934  10978  mulcmpblnr  11016  dedekind  11327  addrid  11344  cnegex  11345  negeu  11400  add20  11676  divdivdiv  11865  ltmul12a  12020  lemul12a  12022  lediv12a  12057  supaddc  12131  supmul1  12133  cru  12154  uzwo3  12877  xleadd1a  13182  xmullem  13193  xmulgt0  13212  xlemul1a  13217  ixxun  13290  ixxss12  13294  ioodisj  13409  fz0fzelfz0  13557  mulexpz  14018  rpexpmord  14083  leexp1a  14090  expmulnbnd  14148  hashf1  14368  fi1uzind  14408  brfi1indALT  14411  swrdccat  14635  reuccatpfxs1  14647  abs3lem  15235  rexanre  15243  cau3lem  15251  limsupgre  15375  limsupbnd2  15377  o1lo1  15431  rlimclim1  15439  rlimclim  15440  rlimcn1  15482  rlimcn3  15484  o1of2  15507  o1rlimmul  15513  lo1add  15521  lo1mul  15522  isercolllem1  15561  climcau  15567  caucvgrlem  15569  caucvgb  15576  summolem2  15612  summo  15613  modfsummod  15690  o1fsum  15709  prodmolem2  15829  addmodlteqALT  16218  rpdvds  16547  isprm5  16594  isprm6  16601  pclem  16721  pcqmul  16736  pcexp  16742  pcneg  16757  pcprmpw2  16765  pcadd  16772  pcmpt  16775  4sqlem13  16840  vdwlem2  16865  vdwlem7  16870  vdwlem12  16875  ramval  16891  ramub2  16897  ramz2  16907  ramcl  16912  cshwshashlem2  16980  imasval  17407  imasdsval  17411  mreexexd  17542  acsfn  17553  issubc3  17749  idfucl  17781  funcres2c  17802  isnat  17848  fucpropd  17880  xpcval  18079  xpcco  18085  prfval  18101  evlf2  18121  evlfcl  18125  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  curf2ndf  18150  hof2val  18159  hofcl  18162  hofpropd  18170  yonedalem4a  18178  yonedainv  18184  drsdirfi  18208  pospo  18248  poslubmo  18314  posglbmo  18315  isipodrs  18440  acsinfd  18459  gsumvalx  18545  gsumpropd2lem  18548  ismndd  18592  mndpropd  18595  mhmeql  18650  mndind  18652  frmdup3lem  18690  mhmmnd  18883  issubg4  18961  ssnmz  18982  conjnmzb  19057  f1otrspeq  19243  psgneu  19302  pgpfi  19401  sylow2blem3  19418  slwhash  19420  fislw  19421  sylow3lem2  19424  lsmdisj2  19478  pj1eu  19492  efgredlem  19543  frgpuplem  19568  gexex  19645  frgpnabl  19667  dprdfadd  19813  dpjidcl  19851  pgpfac1lem3  19870  pgpfaclem3  19876  ablfac2  19882  ablsimpgcygd  19899  ablsimpgfind  19903  ablsimpgprmd  19908  ringpropd  20020  imadrhmcl  20320  islmhm2  20556  lmhmpropd  20591  lbsextlem4  20681  prmirredlem  20930  psgndiflemA  21042  lsmcss  21133  uvcf1  21235  frlmsslsp  21239  frlmup1  21241  assapropd  21312  psrval  21354  evlslem1  21529  mamucl  21785  mamuass  21786  mamudi  21787  mamudir  21788  mamuvs1  21789  mamuvs2  21790  mamulid  21827  mamurid  21828  dmatsubcl  21884  dmatmulcl  21886  scmatscm  21899  marrepval  21948  marepveval  21954  mdetunilem7  22004  gsummatr01lem4  22044  cpmatmcllem  22104  mat2pmatf1  22115  mat2pmatlin  22121  decpmatmul  22158  pm2mpmhmlem2  22205  chpidmat  22233  pptbas  22395  toponmre  22481  restbas  22546  iscncl  22657  cnrest2  22674  cnpdis  22681  lmcnp  22692  dishaus  22770  cmpcovf  22779  tgcmp  22789  dfconn2  22807  clsconn  22818  2ndcctbss  22843  dis2ndc  22848  1stccnp  22850  islly2  22872  cldllycmp  22883  locfincmp  22914  comppfsc  22920  kgentopon  22926  txcls  22992  ptpjopn  23000  dfac14  23006  xkoccn  23007  txcnp  23008  txcmpb  23032  txlm  23036  xkopt  23043  xkoco1cn  23045  xkoco2cn  23046  qtopcn  23102  qtoprest  23105  regr1lem2  23128  xkocnv  23202  qtophmeo  23205  fmfnfmlem4  23345  hausflim  23369  hauspwpwf1  23375  fclscmp  23418  alexsublem  23432  alexsubALTlem2  23436  alexsubALTlem3  23437  ptcmplem3  23442  ptcmplem4  23443  ptcmplem5  23444  cnextfun  23452  tmdgsum2  23484  symgtgp  23494  tsmsval2  23518  tsmsgsum  23527  utoptop  23623  ismet2  23723  blin  23811  metss2lem  23904  methaus  23913  met1stc  23914  met2ndci  23915  prdsxmslem2  23922  metcnp3  23933  metcnpi3  23939  metustto  23946  metustfbas  23950  nlmvscn  24088  nrginvrcn  24093  xrsxmet  24209  reconnlem1  24226  reconn  24228  xrge0tsms  24234  xmetdcn2  24237  metdscn  24256  addcnlem  24264  fsumcn  24270  cnheiborlem  24354  cnheibor  24355  bndth  24358  lebnum  24364  nmoleub2lem2  24516  ipcn  24647  iscmet3  24694  caubl  24709  rrxdstprj1  24810  minveclem3b  24829  minveclem7  24836  pjthlem2  24839  pmltpc  24851  volfiniun  24948  ioombl1  24963  dyadss  24995  dyaddisjlem  24996  dyadmax  24999  dyadmbllem  25000  opnmbllem  25002  itg1addlem2  25098  itg10a  25112  mbfi1fseqlem6  25122  itg2seq  25144  itg2monolem1  25152  itg2gt0  25162  itgfsum  25228  limcfval  25273  ellimc2  25278  ellimc3  25280  limcres  25287  limciun  25295  dvres  25312  dveflem  25380  rolle  25391  dvlip2  25396  c1liplem1  25397  dvgt0lem1  25403  dvgt0  25405  dvlt0  25406  dvne0  25412  dvfsumrlimge0  25431  ftc1lem6  25442  itgsubst  25450  mdegmullem  25480  ply1domn  25525  ply1divex  25538  fta1g  25569  fta1b  25571  plyf  25596  dgrlem  25627  coeid  25636  plydivalg  25696  aannenlem1  25725  aalioulem3  25731  aalioulem6  25734  abelthlem8  25835  efif1olem4  25938  chordthm  26224  xrlimcnp  26355  jensen  26375  lgamcvglem  26426  lgamcvg2  26441  sqf11  26525  fsumvma2  26599  perfectlem2  26615  lgsdilem  26709  lgsquad2lem2  26770  lgsquad3  26772  2sqlem5  26807  2sqlem9  26812  2sqb  26817  rpvmasumlem  26872  dchrisum0flb  26895  dchrisum0  26905  pntpbnd  26973  pntibndlem3  26977  pntleml  26996  nolt02o  27080  nosupbday  27090  nosupbnd2  27101  noinfbday  27105  noinfbnd2  27116  noetasuplem4  27121  noetainflem4  27125  noetalem1  27126  conway  27181  slerec  27201  sltlpss  27279  addsprop  27331  mulsproplem10  27431  tgjustc1  27480  tgjustc2  27481  legov  27590  legtrid  27596  tglinethru  27641  tglnpt2  27646  tglineintmo  27647  mirreu3  27659  perpcom  27718  colperpexlem3  27737  mideu  27743  opphllem1  27752  hlpasch  27761  lnopp2hpgb  27768  trgcopy  27809  brcgr  27912  brbtwn2  27917  colinearalg  27922  axsegcon  27939  axeuclidlem  27974  axcontlem9  27984  ecgrtg  27995  elntg  27996  eengtrkg  27998  upgr1eopALT  28131  usgredg4  28228  subuhgr  28297  subumgr  28299  usgr2wspthon  28973  clwlkclwwlkf1  29017  eupth2lems  29245  n4cyclfrgr  29298  vacn  29699  blocni  29810  ubthlem3  29877  minvecolem7  29888  chocunii  30306  pjhthmo  30307  pjhthlem2  30397  kbass5  31125  mdsymlem5  31412  foresf1o  31495  fcobij  31707  xrofsup  31740  mgcoval  31916  mgcf1o  31933  xrge0tsmsd  31969  symgcntz  32006  archirngz  32095  archiabllem2a  32100  isarchiofld  32183  prmidl2  32289  smatrcl  32466  reff  32509  ordtconnlem1  32594  qqhval2  32652  volmeas  32919  fiunelcarsg  33005  ballotlemfc0  33181  ballotlemfcc  33182  signstfvneq0  33273  derangenlem  33852  erdsze2lem1  33884  pconnconn  33912  connpconn  33916  cvxsconn  33924  cvmliftmolem2  33963  cvmliftmo  33965  cvmlift2lem10  33993  cvmlift2lem12  33995  cvmlift3lem7  34006  mrsubff1  34195  msubff1  34237  ifscgr  34705  cgrxfr  34716  btwnconn1lem13  34760  btwnconn1lem14  34761  outsideofeq  34791  ellines  34813  finminlem  34866  fnejoin2  34917  unbdqndv2  35050  irrdiff  35870  poimirlem13  36164  poimirlem14  36165  poimirlem32  36183  opnmbllem0  36187  mblfinlem3  36190  itg2addnclem  36202  itg2addnc  36205  ftc1cnnc  36223  upixp  36261  filbcmb  36272  sstotbnd2  36306  isbnd3  36316  prdsbnd2  36327  cntotbnd  36328  ismtyima  36335  bfp  36356  rrncmslem  36364  unichnidl  36563  lshpcmp  37523  islshpat  37552  lfl0f  37604  ishlat3N  37889  3dim1  38003  islvol5  38115  lvoli2  38117  lncvrelatN  38317  pclfinclN  38486  pexmidlem8N  38513  idltrn  38686  cdleme42keg  39022  cdleme42mgN  39024  cdlemf2  39098  cdlemg2cex  39127  trlcoat  39259  dihopelvalcpre  39784  dih1dimatlem  39865  dihjatcclem4  39957  lcfl7N  40037  lcfrlem9  40086  mapdh9a  40325  hdmapglem7  40465  aks4d1p8  40617  sticksstones11  40637  imacrhmcl  40762  fsuppind  40823  fsuppssind  40826  mhpind  40827  mhphf  40829  renegeulemv  40895  sn-subeu  40953  remulinvcom  40959  itrere  40993  retire  40994  prjspertr  41001  prjspreln0  41005  flt4lem7  41055  nna4b4nsq  41056  nacsfix  41093  mzpsubst  41129  mzpcompact2lem  41132  eldioph2lem2  41142  eldioph2  41143  eldioph2b  41144  diophin  41153  diophun  41154  irrapxlem3  41205  irrapxlem5  41207  pell1234qrreccl  41235  pell1234qrmulcl  41236  pell14qrdich  41250  pell1qrge1  41251  pell1qrgaplem  41254  monotuz  41323  acongtr  41360  acongrep  41362  jm2.23  41378  jm2.26a  41382  jm2.26lem3  41383  jm2.26  41384  jm2.27  41390  wepwsolem  41427  fnwe2lem2  41436  kelac1  41448  kercvrlsm  41468  hbtlem5  41513  hbt  41515  mpaaeu  41535  cantnfresb  41717  onmcl  41724  tfsconcatun  41730  tfsconcatfn  41731  tfsconcatfv1  41732  tfsconcatfv2  41733  naddcnff  41755  rfovcnvf1od  42398  mnurndlem1  42683  cncmpmax  43359  rfcnnnub  43363  disjxp1  43399  iccintsng  43881  fprodcn  43961  lptioo2  43992  lptioo1  43993  limclner  44012  stoweidlem31  44392  stoweidlem34  44395  stoweidlem35  44396  stoweidlem49  44410  stoweidlem59  44420  stoweidlem62  44423  fourierdlem60  44527  fourierdlem61  44528  fourierdlem87  44554  iundjiun  44821  ismeannd  44828  hoidmvle  44961  smfsuplem2  45173  2reu8i  45465  prproropf1olem2  45816  paireqne  45823  perfectALTVlem2  46034  mogoldbb  46097  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  isomgrtrlem  46150  mgmhmeql  46217  mndpsuppss  46567  scmsuppss  46568  lindslinindsimp2lem5  46663  elfzolborelfzop1  46720  elbigolo1  46763  itschlc0xyqsol1  46972  itschlc0xyqsol  46973  iccdisj  47051  toslat  47127  functhinclem4  47184