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  5097  frpomin  6306  f1imass  7220  f1prex  7240  soisoi  7284  riota5f  7353  frxp3  8103  xpord3pred  8104  tfrlem9a  8327  oeeui  8540  oaabs2  8587  omabs  8589  naddssim  8623  omxpenlem  9018  fopwdom  9025  frfi  9197  marypha1lem  9348  ordiso2  9432  oismo  9457  wemaplem3  9465  cantnf  9614  ttrclss  9641  isinffi  9916  dfac12lem2  10067  dfac12lem3  10068  infxp  10136  infmap2  10139  infpssrlem5  10229  fin23lem11  10239  fin23lem24  10244  fin23lem26  10247  isf32lem2  10276  isf32lem4  10278  fin1a2lem13  10334  fin1a2s  10336  ttukeylem5  10435  fpwwe2lem11  10564  fpwwe2lem12  10565  wunex2  10661  tskord  10703  prlem934  10956  mulcmpblnr  10994  dedekind  11308  addrid  11325  cnegex  11326  negeu  11382  add20  11661  divdivdiv  11854  ltmul12a  12009  lediv12a  12047  cru  12149  uzwo3  12868  xleadd1a  13180  xlemul1a  13215  ixxun  13289  ixxss12  13293  elfz0ubfz0  13560  mulexpz  14037  rpexpmord  14103  leexp1a  14110  expmulnbnd  14170  swrdccatin1  14660  pfxccatin12lem3  14667  pfxccat3  14669  abs3lem  15274  rexanre  15282  cau3lem  15290  lo1bdd2  15459  o1lo1  15472  rlimclim1  15480  rlimclim  15481  lo1resb  15499  o1resb  15501  rlimcn3  15525  o1of2  15548  o1rlimmul  15554  lo1add  15562  lo1mul  15563  isercolllem1  15600  climcau  15606  summolem2  15651  summo  15652  o1fsum  15748  prodmolem2  15870  qredeu  16597  isprm5  16646  pclem  16778  pcqmul  16793  pcexp  16799  pcneg  16814  pcprmpw2  16822  pcadd  16829  prmpwdvds  16844  4sqlem13  16897  vdwlem2  16922  vdwlem7  16927  vdwlem11  16931  vdwlem12  16932  ramval  16948  ramz2  16964  ramcl  16969  prmgaplem6  16996  cshwshashlem2  17036  imasval  17444  imasdsval  17448  mreexexd  17583  issubc3  17785  idfucl  17817  funcres2c  17839  fucpropd  17916  xpcval  18112  prfval  18134  evlfcl  18157  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  curfuncf  18173  curf2ndf  18182  hof2val  18191  hofcl  18194  hofpropd  18202  yonedalem4a  18210  yonedainv  18216  poslubmo  18344  posglbmo  18345  isipodrs  18472  acsmapd  18489  acsinfd  18491  chnpof1  18565  mgmhmeql  18653  sgrppropd  18668  ismndd  18693  mndpropd  18696  mndpsuppss  18702  mhmeql  18763  mndind  18765  frmdup3lem  18803  mhmmnd  19006  issubg4  19087  ssnmz  19107  f1otrspeq  19388  psgneu  19447  sylow2blem3  19563  lsmdisj2  19623  pj1eu  19637  efgredlem  19688  frgpuplem  19713  frgpnabl  19816  dmdprdsplitlem  19980  pgpfac1lem3  20020  pgpfaclem3  20026  ablsimpgcygd  20049  rngpropd  20121  ringpropd  20235  dvdsrtr  20316  rngcinv  20582  ringcinv  20616  islmhm2  21002  lmhmpropd  21037  prmirredlem  21439  psgndiflemA  21568  lsmcss  21659  dsmmlss  21711  uvcf1  21759  frlmup1  21765  assapropd  21839  evlslem1  22049  coe1tmmul2  22230  mamucl  22357  mamuass  22358  mamudi  22359  mamudir  22360  mamuvs1  22361  mamuvs2  22362  mamulid  22397  mamurid  22398  dmatsubcl  22454  dmatmulcl  22456  mdetunilem7  22574  mdetunilem9  22576  cramer0  22646  cpmatmcllem  22674  mat2pmatf1  22685  decpmatmul  22728  pmatcollpw1  22732  pm2mpf1lem  22750  pm2mpmhmlem2  22775  chpidmat  22803  cpmadugsumlemB  22830  cpmadugsumlemC  22831  toponmre  23049  restbas  23114  iscncl  23225  cnpdis  23249  lmcnp  23260  dishaus  23338  cmpcovf  23347  hauscmplem  23362  dfconn2  23375  clsconn  23386  2ndcctbss  23411  1stccnp  23418  islly2  23440  llyidm  23444  cldllycmp  23451  locfincmp  23482  kgentopon  23494  1stckgenlem  23509  ptpjpre1  23527  ptbasfi  23537  txcls  23560  ptpjopn  23568  xkoccn  23575  txcnp  23576  txcmpb  23600  xkoptsub  23610  xkoco2cn  23614  xkoinjcn  23643  qtopcn  23670  qtoprest  23673  regr1lem  23695  regr1lem2  23696  kqreglem1  23697  qtophmeo  23773  fgabs  23835  hauspwpwf1  23943  flimfnfcls  23984  fclscmp  23986  cnpfcf  23997  ptcmplem4  24011  ptcmplem5  24012  cnextfval  24018  cnextfun  24020  tmdgsum2  24052  tsmsval2  24086  utoptop  24190  utop3cls  24207  ismet2  24289  blin  24377  metss2lem  24467  methaus  24476  met1stc  24477  met2ndci  24478  metcnp  24497  metcnpi3  24502  metustto  24509  metustfbas  24513  nlmvscn  24643  nrginvrcn  24648  nghmcn  24701  xrsxmet  24766  reconnlem1  24783  reconn  24785  xrge0tsms  24791  xmetdcn2  24794  metdscn  24813  addcnlem  24821  mulc1cncf  24866  cncfco  24868  cnheiborlem  24921  cnheibor  24922  nmoleub2lem2  25084  ipcn  25214  iscfil3  25241  cfilfcls  25242  iscmet3  25261  caubl  25276  bcthlem5  25296  rrxdstprj1  25377  minveclem3b  25396  minveclem7  25403  pmltpc  25419  ovolshftlem1  25478  ovolscalem1  25482  ioombl1  25531  uniioombllem6  25557  dyadss  25563  dyaddisjlem  25564  dyadmax  25567  opnmbllem  25570  itg1addlem2  25666  itg2seq  25711  bddmulibl  25808  limcfval  25841  ellimc3  25848  limciun  25863  dveflem  25951  rolle  25962  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  dvgt0  25977  dvlt0  25978  dvne0  25984  dvcnvre  25992  dvfsumrlimge0  26005  ftc1lem6  26016  itgsubst  26024  mdegmullem  26051  ply1domn  26097  fta1g  26143  fta1b  26145  dgrlem  26202  coeid  26211  plydivalg  26275  aannenlem1  26304  aalioulem6  26313  ulmcn  26376  mtestbdd  26382  abelthlem8  26417  efif1olem4  26522  chordthm  26815  xrlimcnp  26946  lgamgulmlem5  27011  isppw2  27093  fsumvma2  27193  perfectlem2  27209  lgsdilem  27303  lgsquad2lem2  27364  lgsquad3  27366  2sqlem5  27401  2sqlem9  27406  rpvmasumlem  27466  dchrisum0flb  27489  pntpbnd  27567  pntibndlem3  27571  pntlem3  27588  pntleml  27590  nosupbday  27685  noinfbday  27700  noetasuplem4  27716  noetainflem4  27720  noetalem1  27721  lesrec  27807  madebdaylemlrcut  27907  bdayons  28284  n0fincut  28363  eucliddivs  28384  bdayfinbndlem1  28475  remulscllem2  28509  tgjustc1  28559  tgjustc2  28560  tgbtwnconn1lem3  28658  legtrid  28675  tglinethru  28720  tglnpt2  28725  tglineintmo  28726  mirreu3  28738  perpcom  28797  footexALT  28802  footex  28805  mideu  28822  opphllem1  28831  lnopp2hpgb  28847  axsegcon  29012  axpasch  29026  axeuclidlem  29047  ecgrtg  29068  elntg  29069  eengtrkg  29071  upgr1eopALT  29202  usgredg4  29302  usgr1eop  29335  usgr1v  29341  subuhgr  29371  subumgr  29373  subusgr  29374  nbuhgr2vtx1edgb  29437  wwlksnext  29978  usgr2wspthon  30053  clwlkclwwlkf1  30097  clwwisshclwwslem  30101  n4cyclfrgr  30378  dlwwlknondlwlknonf1o  30452  vacn  30781  ubthlem1  30957  ubthlem3  30959  minvecolem7  30970  chocunii  31388  pjhthmo  31389  pjhthlem2  31479  nmopub2tALT  31996  nmfnleub2  32013  kbass5  32207  mdslmd1lem1  32412  mdslmd1lem2  32413  mdsymlem5  32494  fcobij  32809  xrofsup  32857  mgcf1o  33095  xrge0tsmsd  33166  symgcntz  33178  archiabllem2a  33287  isarchiofld  33292  gsumvsca1  33319  gsumvsca2  33320  prmidl2  33533  ssmxidl  33566  mplvrpmrhm  33723  constrelextdg2  33924  smatrcl  33973  reff  34016  ordtconnlem1  34101  qqhval2  34159  esumpcvgval  34255  imambfm  34439  ballotlemsf1o  34691  signstfvneq0  34749  pconnconn  35444  connpconn  35448  cvmliftmo  35497  cvmlift2lem10  35525  cvmlift2lem12  35527  cvmlift3lem7  35538  mrsubff1  35727  msubff1  35769  ifscgr  36257  cgrxfr  36268  btwnconn1lem13  36312  ellines  36365  weiunso  36679  weiunfr  36680  unblimceq0lem  36725  unbdqndv2  36730  irrdiff  37575  matunitlindflem1  37861  poimirlem4  37869  poimirlem13  37878  poimirlem14  37879  heicant  37900  opnmbllem0  37901  mblfinlem3  37904  itg2addnclem  37916  itg2addnc  37919  ftc1cnnc  37937  sstotbnd  38020  cntotbnd  38041  ismtyima  38048  heibor1lem  38054  heiborlem10  38065  bfp  38069  rrncmslem  38077  islshpsm  39350  lsatcmp  39373  islshpat  39387  lfl0f  39439  iscvlat2N  39694  ishlat3N  39724  3dim1  39837  islvol5  39949  lvoli2  39951  lncvrelatN  40151  lncmp  40153  paddasslem10  40199  pclfinclN  40320  pexmidlem8N  40347  idltrn  40520  cdleme42keg  40856  cdleme42mgN  40858  cdlemf2  40932  cdlemg2cex  40961  trlcoat  41093  tendoex  41345  erngdvlem4  41361  erngdvlem4-rN  41369  dialss  41416  dibglbN  41536  diblss  41540  dihlsscpre  41604  dihglblem2aN  41663  dihglblem4  41667  dihglblem5  41668  dih1dimatlem  41699  dihglblem6  41710  lcfl7N  41871  lcfrlem9  41920  mapdh9a  42159  hdmapglem7  42299  aks4d1p8  42451  isprimroot  42457  evl1gprodd  42481  hashnexinjle  42493  deg1gprod  42504  sticksstones22  42532  grpods  42558  renegeulemv  42732  sn-subeu  42791  remulinvcom  42797  imacrhmcl  42878  fidomncyc  42899  fsuppind  42942  prjspertr  42957  prjspreln0  42961  flt4lem7  43011  nna4b4nsq  43012  isnacs3  43061  nacsfix  43063  mzpsubst  43099  eldioph2lem2  43112  eldioph2  43113  eldioph2b  43114  diophin  43123  diophun  43124  rencldnfilem  43171  irrapxlem3  43175  irrapxlem5  43177  pell1234qrreccl  43205  pell1234qrmulcl  43206  pell1qrge1  43221  pell1qrgaplem  43224  monotuz  43292  monotoddzzfi  43293  acongtr  43329  acongrep  43331  jm2.26a  43351  jm2.26lem3  43352  jm2.26  43353  jm2.27b  43357  jm2.27  43359  wepwsolem  43393  fnwe2lem2  43402  hbtlem5  43479  hbt  43481  mpaaeu  43501  cantnftermord  43671  cantnfresb  43675  omabs2  43683  tfsconcatun  43688  tfsconcatfn  43689  tfsconcatfv1  43690  tfsconcatfv2  43691  tfsconcatfv  43692  tfsconcatrn  43693  naddcnff  43713  oaun3lem1  43725  rfovcnvf1od  44354  mnurndlem1  44631  fnchoice  45383  rfcnnnub  45390  disjxp1  45423  ioondisj2  45847  iccintsng  45877  fprodcn  45954  lptioo2  45985  lptioo1  45986  limclner  46003  dvdsn1add  46291  stoweidlem14  46366  stoweidlem27  46379  stoweidlem34  46386  stoweidlem49  46401  stoweidlem56  46408  fourierdlem87  46545  iundjiun  46812  ismeannd  46819  hoidmvle  46952  prproropf1olem2  47858  perfectALTVlem2  48076  mogoldbb  48139  bgoldbtbndlem2  48160  bgoldbtbndlem3  48161  grimgrtri  48303  isubgr3stgrlem6  48325  rngcinvALTV  48630  ringcinvALTV  48664  lindslinindsimp2lem5  48816  itscnhlinecirc02p  49139  toslat  49335  iinfssclem3  49409  iinfssc  49410  iinfsubc  49411  discsubc  49417  iinfconstbas  49419  imasubc3  49509  upciclem4  49522  natoppf  49582  tposcurf1  49652  fucofvalg  49671  fuco22  49692  fuco22natlem  49698  functhinclem4  49800  functhincfun  49802  arweuthinc  49882  lanfval  49966  ranfval  49967  islmd  50018  iscmd  50019