Theorem simplrl 777

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

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 728	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  5083  frpomin  6298  f1imass  7212  f1prex  7232  soisoi  7276  riota5f  7345  frxp3  8094  xpord3pred  8095  tfrlem9a  8318  oeeui  8531  oaabs2  8578  omabs  8580  naddssim  8614  omxpenlem  9009  fopwdom  9016  frfi  9188  marypha1lem  9339  ordiso2  9423  oismo  9448  wemaplem3  9456  cantnf  9605  ttrclss  9632  isinffi  9907  dfac12lem2  10058  dfac12lem3  10059  infxp  10127  infmap2  10130  infpssrlem5  10220  fin23lem11  10230  fin23lem24  10235  fin23lem26  10238  isf32lem2  10267  isf32lem4  10269  fin1a2lem13  10325  fin1a2s  10327  ttukeylem5  10426  fpwwe2lem11  10555  fpwwe2lem12  10556  wunex2  10652  tskord  10694  prlem934  10947  mulcmpblnr  10985  dedekind  11300  addrid  11317  cnegex  11318  negeu  11374  add20  11653  divdivdiv  11847  ltmul12a  12002  lediv12a  12040  cru  12142  uzwo3  12884  xleadd1a  13196  xlemul1a  13231  ixxun  13305  ixxss12  13309  elfz0ubfz0  13577  mulexpz  14055  rpexpmord  14121  leexp1a  14128  expmulnbnd  14188  swrdccatin1  14678  pfxccatin12lem3  14685  pfxccat3  14687  abs3lem  15292  rexanre  15300  cau3lem  15308  lo1bdd2  15477  o1lo1  15490  rlimclim1  15498  rlimclim  15499  lo1resb  15517  o1resb  15519  rlimcn3  15543  o1of2  15566  o1rlimmul  15572  lo1add  15580  lo1mul  15581  isercolllem1  15618  climcau  15624  summolem2  15669  summo  15670  o1fsum  15767  prodmolem2  15891  qredeu  16618  isprm5  16668  pclem  16800  pcqmul  16815  pcexp  16821  pcneg  16836  pcprmpw2  16844  pcadd  16851  prmpwdvds  16866  4sqlem13  16919  vdwlem2  16944  vdwlem7  16949  vdwlem11  16953  vdwlem12  16954  ramval  16970  ramz2  16986  ramcl  16991  prmgaplem6  17018  cshwshashlem2  17058  imasval  17466  imasdsval  17470  mreexexd  17605  issubc3  17807  idfucl  17839  funcres2c  17861  fucpropd  17938  xpcval  18134  prfval  18156  evlfcl  18179  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  curfuncf  18195  curf2ndf  18204  hof2val  18213  hofcl  18216  hofpropd  18224  yonedalem4a  18232  yonedainv  18238  poslubmo  18366  posglbmo  18367  isipodrs  18494  acsmapd  18511  acsinfd  18513  chnpof1  18587  mgmhmeql  18675  sgrppropd  18690  ismndd  18715  mndpropd  18718  mndpsuppss  18724  mhmeql  18785  mndind  18787  frmdup3lem  18825  mhmmnd  19031  issubg4  19112  ssnmz  19132  f1otrspeq  19413  psgneu  19472  sylow2blem3  19588  lsmdisj2  19648  pj1eu  19662  efgredlem  19713  frgpuplem  19738  frgpnabl  19841  dmdprdsplitlem  20005  pgpfac1lem3  20045  pgpfaclem3  20051  ablsimpgcygd  20074  rngpropd  20146  ringpropd  20260  dvdsrtr  20339  rngcinv  20605  ringcinv  20639  islmhm2  21025  lmhmpropd  21060  prmirredlem  21462  psgndiflemA  21591  lsmcss  21682  dsmmlss  21734  uvcf1  21782  frlmup1  21788  assapropd  21861  evlslem1  22070  coe1tmmul2  22251  mamucl  22376  mamuass  22377  mamudi  22378  mamudir  22379  mamuvs1  22380  mamuvs2  22381  mamulid  22416  mamurid  22417  dmatsubcl  22473  dmatmulcl  22475  mdetunilem7  22593  mdetunilem9  22595  cramer0  22665  cpmatmcllem  22693  mat2pmatf1  22704  decpmatmul  22747  pmatcollpw1  22751  pm2mpf1lem  22769  pm2mpmhmlem2  22794  chpidmat  22822  cpmadugsumlemB  22849  cpmadugsumlemC  22850  toponmre  23068  restbas  23133  iscncl  23244  cnpdis  23268  lmcnp  23279  dishaus  23357  cmpcovf  23366  hauscmplem  23381  dfconn2  23394  clsconn  23405  2ndcctbss  23430  1stccnp  23437  islly2  23459  llyidm  23463  cldllycmp  23470  locfincmp  23501  kgentopon  23513  1stckgenlem  23528  ptpjpre1  23546  ptbasfi  23556  txcls  23579  ptpjopn  23587  xkoccn  23594  txcnp  23595  txcmpb  23619  xkoptsub  23629  xkoco2cn  23633  xkoinjcn  23662  qtopcn  23689  qtoprest  23692  regr1lem  23714  regr1lem2  23715  kqreglem1  23716  qtophmeo  23792  fgabs  23854  hauspwpwf1  23962  flimfnfcls  24003  fclscmp  24005  cnpfcf  24016  ptcmplem4  24030  ptcmplem5  24031  cnextfval  24037  cnextfun  24039  tmdgsum2  24071  tsmsval2  24105  utoptop  24209  utop3cls  24226  ismet2  24308  blin  24396  metss2lem  24486  methaus  24495  met1stc  24496  met2ndci  24497  metcnp  24516  metcnpi3  24521  metustto  24528  metustfbas  24532  nlmvscn  24662  nrginvrcn  24667  nghmcn  24720  xrsxmet  24785  reconnlem1  24802  reconn  24804  xrge0tsms  24810  xmetdcn2  24813  metdscn  24832  addcnlem  24840  mulc1cncf  24882  cncfco  24884  cnheiborlem  24931  cnheibor  24932  nmoleub2lem2  25093  ipcn  25223  iscfil3  25250  cfilfcls  25251  iscmet3  25270  caubl  25285  bcthlem5  25305  rrxdstprj1  25386  minveclem3b  25405  minveclem7  25412  pmltpc  25427  ovolshftlem1  25486  ovolscalem1  25490  ioombl1  25539  uniioombllem6  25565  dyadss  25571  dyaddisjlem  25572  dyadmax  25575  opnmbllem  25578  itg1addlem2  25674  itg2seq  25719  bddmulibl  25816  limcfval  25849  ellimc3  25856  limciun  25871  dveflem  25956  rolle  25967  dvlip2  25972  c1liplem1  25973  dvgt0lem1  25979  dvgt0  25981  dvlt0  25982  dvne0  25988  dvcnvre  25996  dvfsumrlimge0  26007  ftc1lem6  26018  itgsubst  26026  mdegmullem  26053  ply1domn  26099  fta1g  26145  fta1b  26147  dgrlem  26204  coeid  26213  plydivalg  26276  aannenlem1  26305  aalioulem6  26314  ulmcn  26377  mtestbdd  26383  abelthlem8  26417  efif1olem4  26522  chordthm  26814  xrlimcnp  26945  lgamgulmlem5  27010  isppw2  27092  fsumvma2  27191  perfectlem2  27207  lgsdilem  27301  lgsquad2lem2  27362  lgsquad3  27364  2sqlem5  27399  2sqlem9  27404  rpvmasumlem  27464  dchrisum0flb  27487  pntpbnd  27565  pntibndlem3  27569  pntlem3  27586  pntleml  27588  nosupbday  27683  noinfbday  27698  noetasuplem4  27714  noetainflem4  27718  noetalem1  27719  lesrec  27805  madebdaylemlrcut  27905  bdayons  28282  n0fincut  28361  eucliddivs  28382  bdayfinbndlem1  28473  remulscllem2  28507  tgjustc1  28557  tgjustc2  28558  tgbtwnconn1lem3  28656  legtrid  28673  tglinethru  28718  tglnpt2  28723  tglineintmo  28724  mirreu3  28736  perpcom  28795  footexALT  28800  footex  28803  mideu  28820  opphllem1  28829  lnopp2hpgb  28845  axsegcon  29010  axpasch  29024  axeuclidlem  29045  ecgrtg  29066  elntg  29067  eengtrkg  29069  upgr1eopALT  29200  usgredg4  29300  usgr1eop  29333  usgr1v  29339  subuhgr  29369  subumgr  29371  subusgr  29372  nbuhgr2vtx1edgb  29435  wwlksnext  29976  usgr2wspthon  30051  clwlkclwwlkf1  30095  clwwisshclwwslem  30099  n4cyclfrgr  30376  dlwwlknondlwlknonf1o  30450  vacn  30780  ubthlem1  30956  ubthlem3  30958  minvecolem7  30969  chocunii  31387  pjhthmo  31388  pjhthlem2  31478  nmopub2tALT  31995  nmfnleub2  32012  kbass5  32206  mdslmd1lem1  32411  mdslmd1lem2  32412  mdsymlem5  32493  fcobij  32808  xrofsup  32855  mgcf1o  33078  xrge0tsmsd  33149  symgcntz  33161  archiabllem2a  33270  isarchiofld  33275  gsumvsca1  33302  gsumvsca2  33303  prmidl2  33516  ssmxidl  33549  mplvrpmrhm  33706  constrelextdg2  33907  smatrcl  33956  reff  33999  ordtconnlem1  34084  qqhval2  34142  esumpcvgval  34238  imambfm  34422  ballotlemsf1o  34674  signstfvneq0  34732  pconnconn  35429  connpconn  35433  cvmliftmo  35482  cvmlift2lem10  35510  cvmlift2lem12  35512  cvmlift3lem7  35523  mrsubff1  35712  msubff1  35754  ifscgr  36242  cgrxfr  36253  btwnconn1lem13  36297  ellines  36350  weiunso  36664  weiunfr  36665  unblimceq0lem  36782  unbdqndv2  36787  irrdiff  37656  matunitlindflem1  37951  poimirlem4  37959  poimirlem13  37968  poimirlem14  37969  heicant  37990  opnmbllem0  37991  mblfinlem3  37994  itg2addnclem  38006  itg2addnc  38009  ftc1cnnc  38027  sstotbnd  38110  cntotbnd  38131  ismtyima  38138  heibor1lem  38144  heiborlem10  38155  bfp  38159  rrncmslem  38167  islshpsm  39440  lsatcmp  39463  islshpat  39477  lfl0f  39529  iscvlat2N  39784  ishlat3N  39814  3dim1  39927  islvol5  40039  lvoli2  40041  lncvrelatN  40241  lncmp  40243  paddasslem10  40289  pclfinclN  40410  pexmidlem8N  40437  idltrn  40610  cdleme42keg  40946  cdleme42mgN  40948  cdlemf2  41022  cdlemg2cex  41051  trlcoat  41183  tendoex  41435  erngdvlem4  41451  erngdvlem4-rN  41459  dialss  41506  dibglbN  41626  diblss  41630  dihlsscpre  41694  dihglblem2aN  41753  dihglblem4  41757  dihglblem5  41758  dih1dimatlem  41789  dihglblem6  41800  lcfl7N  41961  lcfrlem9  42010  mapdh9a  42249  hdmapglem7  42389  aks4d1p8  42540  isprimroot  42546  evl1gprodd  42570  hashnexinjle  42582  deg1gprod  42593  sticksstones22  42621  grpods  42647  renegeulemv  42814  sn-subeu  42873  remulinvcom  42879  imacrhmcl  42973  fidomncyc  42994  fsuppind  43037  prjspertr  43052  prjspreln0  43056  flt4lem7  43106  nna4b4nsq  43107  isnacs3  43156  nacsfix  43158  mzpsubst  43194  eldioph2lem2  43207  eldioph2  43208  eldioph2b  43209  diophin  43218  diophun  43219  rencldnfilem  43266  irrapxlem3  43270  irrapxlem5  43272  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell1qrge1  43316  pell1qrgaplem  43319  monotuz  43387  monotoddzzfi  43388  acongtr  43424  acongrep  43426  jm2.26a  43446  jm2.26lem3  43447  jm2.26  43448  jm2.27b  43452  jm2.27  43454  wepwsolem  43488  fnwe2lem2  43497  hbtlem5  43574  hbt  43576  mpaaeu  43596  cantnftermord  43766  cantnfresb  43770  omabs2  43778  tfsconcatun  43783  tfsconcatfn  43784  tfsconcatfv1  43785  tfsconcatfv2  43786  tfsconcatfv  43787  tfsconcatrn  43788  naddcnff  43808  oaun3lem1  43820  rfovcnvf1od  44449  mnurndlem1  44726  fnchoice  45478  rfcnnnub  45485  disjxp1  45518  ioondisj2  45941  iccintsng  45971  fprodcn  46048  lptioo2  46079  lptioo1  46080  limclner  46097  dvdsn1add  46385  stoweidlem14  46460  stoweidlem27  46473  stoweidlem34  46480  stoweidlem49  46495  stoweidlem56  46502  fourierdlem87  46639  iundjiun  46906  ismeannd  46913  hoidmvle  47046  prproropf1olem2  47976  nprmmul2  48000  perfectALTVlem2  48210  mogoldbb  48273  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  grimgrtri  48437  isubgr3stgrlem6  48459  rngcinvALTV  48764  ringcinvALTV  48798  lindslinindsimp2lem5  48950  itscnhlinecirc02p  49273  toslat  49469  iinfssclem3  49543  iinfssc  49544  iinfsubc  49545  discsubc  49551  iinfconstbas  49553  imasubc3  49643  upciclem4  49656  natoppf  49716  tposcurf1  49786  fucofvalg  49805  fuco22  49826  fuco22natlem  49832  functhinclem4  49934  functhincfun  49936  arweuthinc  50016  lanfval  50100  ranfval  50101  islmd  50152  iscmd  50153