Theorem simplrr 790

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5099  frpomin  6343  fsnex  7291  f1prex  7292  isotr  7344  weniso  7364  riota5f  7405  fnwe2lem3  8147  frxp2  8161  frxp3  8168  xpord3pred  8169  poseq  8175  fprlem2  8319  tfrlem9a  8394  oaass  8569  oeeui  8611  oaabs2  8658  coflton  8680  cofon1  8681  naddssim  8695  resixpfo  8964  omxpenlem  9097  pw2f1olem  9100  fopwdom  9104  fofinf1o  9321  marypha1lem  9425  ordiso2  9509  oismo  9534  ixpiunwdom  9584  cantnf  9694  ttrclss  9721  fseqenlem1  10103  iunfictbso  10193  dfac12lem2  10223  dfac12lem3  10224  infunsdom1  10290  infpssrlem5  10385  fin23lem24  10400  isf32lem2  10432  isf32lem4  10434  isf34lem4  10455  fin1a2lem12  10489  fin1a2lem13  10490  ttukeylem6  10592  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  winalim2  10781  wunex2  10823  tskord  10865  prlem934  11118  mulcmpblnr  11156  dedekind  11473  addrid  11490  cnegex  11491  negeu  11547  add20  11828  divdivdiv  12018  ltmul12a  12173  lemul12a  12175  lediv12a  12210  supaddc  12284  supmul1  12286  cru  12312  uzwo3  13070  xleadd1a  13383  xmullem  13394  xmulgt0  13413  xlemul1a  13418  ixxun  13492  ixxss12  13496  ioodisj  13613  fz0fzelfz0  13768  mulexpz  14245  rpexpmord  14311  leexp1a  14318  expmulnbnd  14379  hashf1  14602  fi1uzind  14652  brfi1indALT  14655  swrdccat  14884  reuccatpfxs1  14896  abs3lem  15506  rexanre  15514  cau3lem  15522  limsupgre  15648  limsupbnd2  15650  o1lo1  15704  rlimclim1  15712  rlimclim  15713  rlimcn1  15755  rlimcn3  15757  o1of2  15780  o1rlimmul  15786  lo1add  15794  lo1mul  15795  isercolllem1  15832  climcau  15838  caucvgrlem  15840  caucvgb  15847  summolem2  15882  summo  15883  modfsummod  15961  o1fsum  15980  prodmolem2  16102  addmodlteqALT  16495  rpdvds  16835  isprm5  16883  isprm6  16890  pclem  17016  pcqmul  17031  pcexp  17037  pcneg  17052  pcprmpw2  17060  pcadd  17067  pcmpt  17070  4sqlem13  17135  vdwlem2  17160  vdwlem7  17165  vdwlem12  17170  ramval  17186  ramub2  17192  ramz2  17202  ramcl  17207  cshwshashlem2  17274  imasval  17683  imasdsval  17687  mreexexd  17822  acsfn  17833  issubc3  18024  idfucl  18056  funcres2c  18078  isnat  18125  fucpropd  18155  xpcval  18351  xpcco  18357  prfval  18373  evlf2  18392  evlfcl  18396  curf12  18401  curf1cl  18402  curf2  18403  curfcl  18406  curf2ndf  18421  hof2val  18430  hofcl  18433  hofpropd  18441  yonedalem4a  18449  yonedainv  18455  drsdirfi  18479  pospo  18517  poslubmo  18583  posglbmo  18584  isipodrs  18711  acsinfd  18730  chnccat  18800  chnpof1  18804  gsumvalx  18865  gsumpropd2lem  18868  mgmhmeql  18905  sgrppropd  18920  ismndd  18946  mndpropd  18951  mndpsuppss  18959  mhmeql  19022  mndind  19024  frmdup3lem  19062  mhmmnd  19274  issubg4  19356  ssnmz  19376  conjnmzb  19467  f1otrspeq  19661  psgneu  19720  pgpfi  19819  sylow2blem3  19836  slwhash  19838  fislw  19839  sylow3lem2  19842  lsmdisj2  19896  pj1eu  19910  efgredlem  19961  frgpuplem  19986  gexex  20067  frgpnabl  20089  dprdfadd  20236  dpjidcl  20274  pgpfac1lem3  20293  pgpfaclem3  20299  ablfac2  20305  ablsimpgcygd  20322  ablsimpgfind  20326  ablsimpgprmd  20331  rngpropd  20396  ringpropd  20519  imadrhmcl  21054  islmhm2  21313  lmhmpropd  21348  lbsextlem4  21439  prmidl2  21622  prmirredlem  21778  psgndiflemA  21907  lsmcss  21998  uvcf1  22098  frlmsslsp  22102  frlmup1  22104  assapropd  22179  psrval  22223  evlslem1  22391  mamucl  22716  mamuass  22717  mamudi  22718  mamudir  22719  mamuvs1  22720  mamuvs2  22721  mamulid  22756  mamurid  22757  dmatsubcl  22813  dmatmulcl  22815  scmatscm  22828  marrepval  22877  marepveval  22883  mdetunilem7  22933  gsummatr01lem4  22973  cpmatmcllem  23036  mat2pmatf1  23047  mat2pmatlin  23053  decpmatmul  23090  pm2mpmhmlem2  23137  chpidmat  23165  pptbas  23326  toponmre  23411  restbas  23476  iscncl  23587  cnrest2  23604  cnpdis  23611  lmcnp  23622  dishaus  23700  cmpcovf  23709  tgcmp  23719  dfconn2  23737  clsconn  23748  2ndcctbss  23774  dis2ndc  23779  1stccnp  23781  islly2  23803  cldllycmp  23814  locfincmp  23845  comppfsc  23851  kgentopon  23857  txcls  23923  ptpjopn  23931  dfac14  23937  xkoccn  23938  txcnp  23939  txcmpb  23963  txlm  23967  xkopt  23974  xkoco1cn  23976  xkoco2cn  23977  qtopcn  24033  qtoprest  24036  regr1lem2  24059  xkocnv  24133  qtophmeo  24136  fmfnfmlem4  24276  hausflim  24300  hauspwpwf1  24306  fclscmp  24349  alexsublem  24363  alexsubALTlem2  24367  alexsubALTlem3  24368  ptcmplem3  24373  ptcmplem4  24374  ptcmplem5  24375  cnextfun  24383  tmdgsum2  24415  symgtgp  24425  tsmsval2  24449  tsmsgsum  24458  utoptop  24553  ismet2  24652  blin  24740  metss2lem  24830  methaus  24839  met1stc  24840  met2ndci  24841  prdsxmslem2  24848  metcnp3  24859  metcnpi3  24865  metustto  24872  metustfbas  24876  nlmvscn  25006  nrginvrcn  25011  xrsxmet  25129  reconnlem1  25146  reconn  25148  xrge0tsms  25154  xmetdcn2  25157  metdscn  25176  addcnlem  25184  fsumcn  25191  cnheiborlem  25275  cnheibor  25276  bndth  25279  lebnum  25285  nmoleub2lem2  25437  ipcn  25567  iscmet3  25614  caubl  25629  rrxdstprj1  25730  minveclem3b  25749  minveclem7  25756  pjthlem2  25759  pmltpc  25771  volfiniun  25868  ioombl1  25883  dyadss  25915  dyaddisjlem  25916  dyadmax  25919  dyadmbllem  25920  opnmbllem  25922  itg1addlem2  26018  itg10a  26031  mbfi1fseqlem6  26041  itg2seq  26063  itg2monolem1  26071  itg2gt0  26081  itgfsum  26147  limcfval  26192  ellimc2  26197  ellimc3  26199  limcres  26206  limciun  26214  dvres  26231  dveflem  26299  rolle  26310  dvlip2  26315  c1liplem1  26316  dvgt0lem1  26322  dvgt0  26324  dvlt0  26325  dvne0  26331  dvfsumrlimge0  26350  ftc1lem6  26361  itgsubst  26369  mdegmullem  26396  ply1domn  26442  ply1divex  26455  fta1g  26488  fta1b  26490  plyf  26516  dgrlem  26548  coeid  26557  plydivalg  26620  aannenlem1  26655  aalioulem3  26661  aalioulem6  26664  abelthlem8  26766  efif1olem4  26873  chordthm  27165  xrlimcnp  27296  jensen  27316  lgamcvglem  27367  lgamcvg2  27382  sqf11  27466  fsumvma2  27541  perfectlem2  27557  lgsdilem  27651  lgsquad2lem2  27712  lgsquad3  27714  2sqlem5  27749  2sqlem9  27754  2sqb  27759  rpvmasumlem  27814  dchrisum0flb  27837  dchrisum0  27847  pntpbnd  27915  pntibndlem3  27919  pntleml  27938  flt4lem7  27989  nna4b4nsq  27990  nolt02o  28052  nosupbday  28062  nosupbnd2  28073  noinfbday  28077  noinfbnd2  28088  noetasuplem4  28093  noetainflem4  28097  noetalem1  28098  conway  28165  lesrec  28185  ltslpss  28294  addsprop  28362  bdayons  28662  n0fincut  28741  eucliddivs  28762  remulscllem2  28887  tgjustc1  28937  tgjustc2  28938  legov  29048  legtrid  29054  tglinethru  29104  tglineintmo  29110  tglnpt2  29121  mirreu3  29126  perpcom  29188  colperpexlem3  29208  mideu  29214  opphllem1  29223  hlpasch  29234  lnopp2hpgb  29241  trgcopy  29311  brcgr  29478  brbtwn2  29483  colinearalg  29488  axsegcon  29505  axeuclidlem  29540  axcontlem9  29550  ecgrtg  29561  elntg  29562  eengtrkg  29564  upgr1eopALT  29695  usgredg4  29798  subuhgr  29867  subumgr  29869  usgr2wspthon  30557  clwlkclwwlkf1  30601  eupth2lems  30839  n4cyclfrgr  30892  vacn  31296  blocni  31407  ubthlem3  31474  minvecolem7  31485  chocunii  31903  pjhthmo  31904  pjhthlem2  31994  kbass5  32722  mdsymlem5  33009  foresf1o  33142  fcobij  33354  xrofsup  33401  mgcoval  33589  mgcf1o  33606  xrge0tsmsd  33676  symgcntz  33688  archirngz  33792  archiabllem2a  33797  isarchiofld  33802  mplvrpmmhm  34220  constrelextdg2  34421  smatrcl  34470  reff  34513  ordtconnlem1  34598  qqhval2  34656  volmeas  34906  fiunelcarsg  34990  ballotlemfc0  35167  ballotlemfcc  35168  signstfvneq0  35243  derangenlem  35978  erdsze2lem1  36010  pconnconn  36038  connpconn  36042  cvxsconn  36050  cvmliftmolem2  36089  cvmliftmo  36091  cvmlift2lem10  36119  cvmlift2lem12  36121  cvmlift3lem7  36132  mrsubff1  36321  msubff1  36363  r1peuqusdeg1  36450  ifscgr  36851  cgrxfr  36862  btwnconn1lem13  36906  btwnconn1lem14  36907  outsideofeq  36937  ellines  36959  nadddilem4  37014  finminlem  37148  fnejoin2  37199  weiunso  37296  unbdqndv2  37419  irrdiff  38290  qdiff  38291  poimirlem13  38594  poimirlem14  38595  poimirlem32  38613  opnmbllem0  38617  mblfinlem3  38620  itg2addnclem  38632  itg2addnc  38635  ftc1cnnc  38653  upixp  38706  filbcmb  38717  sstotbnd2  38751  isbnd3  38761  prdsbnd2  38772  cntotbnd  38773  ismtyima  38780  bfp  38801  rrncmslem  38809  unichnidl  39008  lshpcmp  40088  islshpat  40117  lfl0f  40169  ishlat3N  40454  3dim1  40567  islvol5  40679  lvoli2  40681  lncvrelatN  40881  pclfinclN  41050  pexmidlem8N  41077  idltrn  41250  cdleme42keg  41586  cdleme42mgN  41588  cdlemf2  41662  cdlemg2cex  41691  trlcoat  41823  dihopelvalcpre  42348  dih1dimatlem  42429  dihjatcclem4  42521  lcfl7N  42601  lcfrlem9  42650  mapdh9a  42889  hdmapglem7  43029  aks4d1p8  43180  isprimroot  43186  evl1gprodd  43210  sticksstones11  43249  grpods  43287  aks5lem8  43294  renegeulemv  43462  sn-subeu  43521  remulinvcom  43527  imacrhmcl  43624  fidomncyc  43642  fsuppind  43661  fsuppssind  43664  mhpind  43665  prjspertr  43676  prjspreln0  43680  nacsfix  43766  mzpsubst  43802  mzpcompact2lem  43805  eldioph2lem2  43815  eldioph2  43816  eldioph2b  43817  diophin  43826  diophun  43827  irrapxlem3  43874  irrapxlem5  43876  pell1234qrreccl  43904  pell1234qrmulcl  43905  pell14qrdich  43919  pell1qrge1  43920  pell1qrgaplem  43923  monotuz  43991  acongtr  44028  acongrep  44030  jm2.23  44046  jm2.26a  44050  jm2.26lem3  44051  jm2.26  44052  jm2.27  44058  wepwsolem  44092  kelac1  44108  kercvrlsm  44128  hbtlem5  44173  hbt  44175  mpaaeu  44195  cantnfresb  44369  onmcl  44376  tfsconcatun  44382  tfsconcatfn  44383  tfsconcatfv1  44384  tfsconcatfv2  44385  naddcnff  44407  rfovcnvf1od  45047  mnurndlem1  45308  cncmpmax  46092  rfcnnnub  46096  disjxp1  46129  iccintsng  46578  fprodcn  46655  lptioo2  46686  lptioo1  46687  limclner  46704  stoweidlem31  47084  stoweidlem34  47087  stoweidlem35  47088  stoweidlem49  47102  stoweidlem59  47112  stoweidlem62  47115  fourierdlem60  47219  fourierdlem61  47220  fourierdlem87  47246  iundjiun  47513  ismeannd  47520  hoidmvle  47653  smfsuplem2  47865  2reu8i  48226  prproropf1olem2  48629  paireqne  48636  nprmmul2  48653  perfectALTVlem2  48863  mogoldbb  48926  bgoldbtbndlem2  48947  bgoldbtbndlem3  48948  grimedg  49076  grlimprclnbgrvtx  49140  scmsuppss  49526  lindslinindsimp2lem5  49617  elfzolborelfzop1  49674  elbigolo1  49712  itschlc0xyqsol1  49921  itschlc0xyqsol  49922  iccdisj  50049  toslat  50133  iinfssclem3  50207  iinfssc  50208  iinfsubc  50209  imasubc3  50307  upciclem4  50320  uppropd  50332  natoppf  50380  tposcurf1  50450  fuco22  50490  fuco22natlem  50496  functhinclem4  50598  arweuthinc  50680