Theorem simplrl 776

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 727	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  5095  frpomin  6298  f1imass  7210  f1prex  7230  soisoi  7274  riota5f  7343  frxp3  8093  xpord3pred  8094  tfrlem9a  8317  oeeui  8530  oaabs2  8577  omabs  8579  naddssim  8613  omxpenlem  9006  fopwdom  9013  frfi  9185  marypha1lem  9336  ordiso2  9420  oismo  9445  wemaplem3  9453  cantnf  9602  ttrclss  9629  isinffi  9904  dfac12lem2  10055  dfac12lem3  10056  infxp  10124  infmap2  10127  infpssrlem5  10217  fin23lem11  10227  fin23lem24  10232  fin23lem26  10235  isf32lem2  10264  isf32lem4  10266  fin1a2lem13  10322  fin1a2s  10324  ttukeylem5  10423  fpwwe2lem11  10552  fpwwe2lem12  10553  wunex2  10649  tskord  10691  prlem934  10944  mulcmpblnr  10982  dedekind  11296  addrid  11313  cnegex  11314  negeu  11370  add20  11649  divdivdiv  11842  ltmul12a  11997  lediv12a  12035  cru  12137  uzwo3  12856  xleadd1a  13168  xlemul1a  13203  ixxun  13277  ixxss12  13281  elfz0ubfz0  13548  mulexpz  14025  rpexpmord  14091  leexp1a  14098  expmulnbnd  14158  swrdccatin1  14648  pfxccatin12lem3  14655  pfxccat3  14657  abs3lem  15262  rexanre  15270  cau3lem  15278  lo1bdd2  15447  o1lo1  15460  rlimclim1  15468  rlimclim  15469  lo1resb  15487  o1resb  15489  rlimcn3  15513  o1of2  15536  o1rlimmul  15542  lo1add  15550  lo1mul  15551  isercolllem1  15588  climcau  15594  summolem2  15639  summo  15640  o1fsum  15736  prodmolem2  15858  qredeu  16585  isprm5  16634  pclem  16766  pcqmul  16781  pcexp  16787  pcneg  16802  pcprmpw2  16810  pcadd  16817  prmpwdvds  16832  4sqlem13  16885  vdwlem2  16910  vdwlem7  16915  vdwlem11  16919  vdwlem12  16920  ramval  16936  ramz2  16952  ramcl  16957  prmgaplem6  16984  cshwshashlem2  17024  imasval  17432  imasdsval  17436  mreexexd  17571  issubc3  17773  idfucl  17805  funcres2c  17827  fucpropd  17904  xpcval  18100  prfval  18122  evlfcl  18145  curf12  18150  curf1cl  18151  curf2  18152  curfcl  18155  curfuncf  18161  curf2ndf  18170  hof2val  18179  hofcl  18182  hofpropd  18190  yonedalem4a  18198  yonedainv  18204  poslubmo  18332  posglbmo  18333  isipodrs  18460  acsmapd  18477  acsinfd  18479  chnpof1  18553  mgmhmeql  18641  sgrppropd  18656  ismndd  18681  mndpropd  18684  mndpsuppss  18690  mhmeql  18751  mndind  18753  frmdup3lem  18791  mhmmnd  18994  issubg4  19075  ssnmz  19095  f1otrspeq  19376  psgneu  19435  sylow2blem3  19551  lsmdisj2  19611  pj1eu  19625  efgredlem  19676  frgpuplem  19701  frgpnabl  19804  dmdprdsplitlem  19968  pgpfac1lem3  20008  pgpfaclem3  20014  ablsimpgcygd  20037  rngpropd  20109  ringpropd  20223  dvdsrtr  20304  rngcinv  20570  ringcinv  20604  islmhm2  20990  lmhmpropd  21025  prmirredlem  21427  psgndiflemA  21556  lsmcss  21647  dsmmlss  21699  uvcf1  21747  frlmup1  21753  assapropd  21827  evlslem1  22037  coe1tmmul2  22218  mamucl  22345  mamuass  22346  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  mamulid  22385  mamurid  22386  dmatsubcl  22442  dmatmulcl  22444  mdetunilem7  22562  mdetunilem9  22564  cramer0  22634  cpmatmcllem  22662  mat2pmatf1  22673  decpmatmul  22716  pmatcollpw1  22720  pm2mpf1lem  22738  pm2mpmhmlem2  22763  chpidmat  22791  cpmadugsumlemB  22818  cpmadugsumlemC  22819  toponmre  23037  restbas  23102  iscncl  23213  cnpdis  23237  lmcnp  23248  dishaus  23326  cmpcovf  23335  hauscmplem  23350  dfconn2  23363  clsconn  23374  2ndcctbss  23399  1stccnp  23406  islly2  23428  llyidm  23432  cldllycmp  23439  locfincmp  23470  kgentopon  23482  1stckgenlem  23497  ptpjpre1  23515  ptbasfi  23525  txcls  23548  ptpjopn  23556  xkoccn  23563  txcnp  23564  txcmpb  23588  xkoptsub  23598  xkoco2cn  23602  xkoinjcn  23631  qtopcn  23658  qtoprest  23661  regr1lem  23683  regr1lem2  23684  kqreglem1  23685  qtophmeo  23761  fgabs  23823  hauspwpwf1  23931  flimfnfcls  23972  fclscmp  23974  cnpfcf  23985  ptcmplem4  23999  ptcmplem5  24000  cnextfval  24006  cnextfun  24008  tmdgsum2  24040  tsmsval2  24074  utoptop  24178  utop3cls  24195  ismet2  24277  blin  24365  metss2lem  24455  methaus  24464  met1stc  24465  met2ndci  24466  metcnp  24485  metcnpi3  24490  metustto  24497  metustfbas  24501  nlmvscn  24631  nrginvrcn  24636  nghmcn  24689  xrsxmet  24754  reconnlem1  24771  reconn  24773  xrge0tsms  24779  xmetdcn2  24782  metdscn  24801  addcnlem  24809  mulc1cncf  24854  cncfco  24856  cnheiborlem  24909  cnheibor  24910  nmoleub2lem2  25072  ipcn  25202  iscfil3  25229  cfilfcls  25230  iscmet3  25249  caubl  25264  bcthlem5  25284  rrxdstprj1  25365  minveclem3b  25384  minveclem7  25391  pmltpc  25407  ovolshftlem1  25466  ovolscalem1  25470  ioombl1  25519  uniioombllem6  25545  dyadss  25551  dyaddisjlem  25552  dyadmax  25555  opnmbllem  25558  itg1addlem2  25654  itg2seq  25699  bddmulibl  25796  limcfval  25829  ellimc3  25836  limciun  25851  dveflem  25939  rolle  25950  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  dvgt0  25965  dvlt0  25966  dvne0  25972  dvcnvre  25980  dvfsumrlimge0  25993  ftc1lem6  26004  itgsubst  26012  mdegmullem  26039  ply1domn  26085  fta1g  26131  fta1b  26133  dgrlem  26190  coeid  26199  plydivalg  26263  aannenlem1  26292  aalioulem6  26301  ulmcn  26364  mtestbdd  26370  abelthlem8  26405  efif1olem4  26510  chordthm  26803  xrlimcnp  26934  lgamgulmlem5  26999  isppw2  27081  fsumvma2  27181  perfectlem2  27197  lgsdilem  27291  lgsquad2lem2  27352  lgsquad3  27354  2sqlem5  27389  2sqlem9  27394  rpvmasumlem  27454  dchrisum0flb  27477  pntpbnd  27555  pntibndlem3  27559  pntlem3  27576  pntleml  27578  nosupbday  27673  noinfbday  27688  noetasuplem4  27704  noetainflem4  27708  noetalem1  27709  lesrec  27795  madebdaylemlrcut  27895  bdayons  28272  n0fincut  28351  eucliddivs  28372  bdayfinbndlem1  28463  remulscllem2  28497  tgjustc1  28547  tgjustc2  28548  tgbtwnconn1lem3  28646  legtrid  28663  tglinethru  28708  tglnpt2  28713  tglineintmo  28714  mirreu3  28726  perpcom  28785  footexALT  28790  footex  28793  mideu  28810  opphllem1  28819  lnopp2hpgb  28835  axsegcon  29000  axpasch  29014  axeuclidlem  29035  ecgrtg  29056  elntg  29057  eengtrkg  29059  upgr1eopALT  29190  usgredg4  29290  usgr1eop  29323  usgr1v  29329  subuhgr  29359  subumgr  29361  subusgr  29362  nbuhgr2vtx1edgb  29425  wwlksnext  29966  usgr2wspthon  30041  clwlkclwwlkf1  30085  clwwisshclwwslem  30089  n4cyclfrgr  30366  dlwwlknondlwlknonf1o  30440  vacn  30769  ubthlem1  30945  ubthlem3  30947  minvecolem7  30958  chocunii  31376  pjhthmo  31377  pjhthlem2  31467  nmopub2tALT  31984  nmfnleub2  32001  kbass5  32195  mdslmd1lem1  32400  mdslmd1lem2  32401  mdsymlem5  32482  fcobij  32799  xrofsup  32847  mgcf1o  33085  xrge0tsmsd  33155  symgcntz  33167  archiabllem2a  33276  isarchiofld  33281  gsumvsca1  33308  gsumvsca2  33309  prmidl2  33522  ssmxidl  33555  mplvrpmrhm  33712  constrelextdg2  33904  smatrcl  33953  reff  33996  ordtconnlem1  34081  qqhval2  34139  esumpcvgval  34235  imambfm  34419  ballotlemsf1o  34671  signstfvneq0  34729  pconnconn  35425  connpconn  35429  cvmliftmo  35478  cvmlift2lem10  35506  cvmlift2lem12  35508  cvmlift3lem7  35519  mrsubff1  35708  msubff1  35750  ifscgr  36238  cgrxfr  36249  btwnconn1lem13  36293  ellines  36346  weiunso  36660  weiunfr  36661  unblimceq0lem  36706  unbdqndv2  36711  irrdiff  37527  matunitlindflem1  37813  poimirlem4  37821  poimirlem13  37830  poimirlem14  37831  heicant  37852  opnmbllem0  37853  mblfinlem3  37856  itg2addnclem  37868  itg2addnc  37871  ftc1cnnc  37889  sstotbnd  37972  cntotbnd  37993  ismtyima  38000  heibor1lem  38006  heiborlem10  38017  bfp  38021  rrncmslem  38029  islshpsm  39236  lsatcmp  39259  islshpat  39273  lfl0f  39325  iscvlat2N  39580  ishlat3N  39610  3dim1  39723  islvol5  39835  lvoli2  39837  lncvrelatN  40037  lncmp  40039  paddasslem10  40085  pclfinclN  40206  pexmidlem8N  40233  idltrn  40406  cdleme42keg  40742  cdleme42mgN  40744  cdlemf2  40818  cdlemg2cex  40847  trlcoat  40979  tendoex  41231  erngdvlem4  41247  erngdvlem4-rN  41255  dialss  41302  dibglbN  41422  diblss  41426  dihlsscpre  41490  dihglblem2aN  41549  dihglblem4  41553  dihglblem5  41554  dih1dimatlem  41585  dihglblem6  41596  lcfl7N  41757  lcfrlem9  41806  mapdh9a  42045  hdmapglem7  42185  aks4d1p8  42337  isprimroot  42343  evl1gprodd  42367  hashnexinjle  42379  deg1gprod  42390  sticksstones22  42418  grpods  42444  renegeulemv  42619  sn-subeu  42678  remulinvcom  42684  imacrhmcl  42765  fidomncyc  42786  fsuppind  42829  prjspertr  42844  prjspreln0  42848  flt4lem7  42898  nna4b4nsq  42899  isnacs3  42948  nacsfix  42950  mzpsubst  42986  eldioph2lem2  42999  eldioph2  43000  eldioph2b  43001  diophin  43010  diophun  43011  rencldnfilem  43058  irrapxlem3  43062  irrapxlem5  43064  pell1234qrreccl  43092  pell1234qrmulcl  43093  pell1qrge1  43108  pell1qrgaplem  43111  monotuz  43179  monotoddzzfi  43180  acongtr  43216  acongrep  43218  jm2.26a  43238  jm2.26lem3  43239  jm2.26  43240  jm2.27b  43244  jm2.27  43246  wepwsolem  43280  fnwe2lem2  43289  hbtlem5  43366  hbt  43368  mpaaeu  43388  cantnftermord  43558  cantnfresb  43562  omabs2  43570  tfsconcatun  43575  tfsconcatfn  43576  tfsconcatfv1  43577  tfsconcatfv2  43578  tfsconcatfv  43579  tfsconcatrn  43580  naddcnff  43600  oaun3lem1  43612  rfovcnvf1od  44241  mnurndlem1  44518  fnchoice  45270  rfcnnnub  45277  disjxp1  45310  ioondisj2  45735  iccintsng  45765  fprodcn  45842  lptioo2  45873  lptioo1  45874  limclner  45891  dvdsn1add  46179  stoweidlem14  46254  stoweidlem27  46267  stoweidlem34  46274  stoweidlem49  46289  stoweidlem56  46296  fourierdlem87  46433  iundjiun  46700  ismeannd  46707  hoidmvle  46840  prproropf1olem2  47746  perfectALTVlem2  47964  mogoldbb  48027  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  grimgrtri  48191  isubgr3stgrlem6  48213  rngcinvALTV  48518  ringcinvALTV  48552  lindslinindsimp2lem5  48704  itscnhlinecirc02p  49027  toslat  49223  iinfssclem3  49297  iinfssc  49298  iinfsubc  49299  discsubc  49305  iinfconstbas  49307  imasubc3  49397  upciclem4  49410  natoppf  49470  tposcurf1  49540  fucofvalg  49559  fuco22  49580  fuco22natlem  49586  functhinclem4  49688  functhincfun  49690  arweuthinc  49770  lanfval  49854  ranfval  49855  islmd  49906  iscmd  49907