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  5107  frpomin  6316  f1imass  7242  f1prex  7262  soisoi  7306  riota5f  7375  frxp3  8133  xpord3pred  8134  tfrlem9a  8357  oeeui  8569  oaabs2  8616  omabs  8618  naddssim  8652  omxpenlem  9047  fopwdom  9054  frfi  9239  marypha1lem  9391  ordiso2  9475  oismo  9500  wemaplem3  9508  cantnf  9653  ttrclss  9680  isinffi  9952  dfac12lem2  10105  dfac12lem3  10106  infxp  10174  infmap2  10177  infpssrlem5  10267  fin23lem11  10277  fin23lem24  10282  fin23lem26  10285  isf32lem2  10314  isf32lem4  10316  fin1a2lem13  10372  fin1a2s  10374  ttukeylem5  10473  fpwwe2lem11  10601  fpwwe2lem12  10602  wunex2  10698  tskord  10740  prlem934  10993  mulcmpblnr  11031  dedekind  11344  addrid  11361  cnegex  11362  negeu  11418  add20  11697  divdivdiv  11890  ltmul12a  12045  lediv12a  12083  cru  12185  uzwo3  12909  xleadd1a  13220  xlemul1a  13255  ixxun  13329  ixxss12  13333  elfz0ubfz0  13600  mulexpz  14074  rpexpmord  14140  leexp1a  14147  expmulnbnd  14207  swrdccatin1  14697  pfxccatin12lem3  14704  pfxccat3  14706  abs3lem  15312  rexanre  15320  cau3lem  15328  lo1bdd2  15497  o1lo1  15510  rlimclim1  15518  rlimclim  15519  lo1resb  15537  o1resb  15539  rlimcn3  15563  o1of2  15586  o1rlimmul  15592  lo1add  15600  lo1mul  15601  isercolllem1  15638  climcau  15644  summolem2  15689  summo  15690  o1fsum  15786  prodmolem2  15908  qredeu  16635  isprm5  16684  pclem  16816  pcqmul  16831  pcexp  16837  pcneg  16852  pcprmpw2  16860  pcadd  16867  prmpwdvds  16882  4sqlem13  16935  vdwlem2  16960  vdwlem7  16965  vdwlem11  16969  vdwlem12  16970  ramval  16986  ramz2  17002  ramcl  17007  prmgaplem6  17034  cshwshashlem2  17074  imasval  17481  imasdsval  17485  mreexexd  17616  issubc3  17818  idfucl  17850  funcres2c  17872  fucpropd  17949  xpcval  18145  prfval  18167  evlfcl  18190  curf12  18195  curf1cl  18196  curf2  18197  curfcl  18200  curfuncf  18206  curf2ndf  18215  hof2val  18224  hofcl  18227  hofpropd  18235  yonedalem4a  18243  yonedainv  18249  poslubmo  18377  posglbmo  18378  isipodrs  18503  acsmapd  18520  acsinfd  18522  mgmhmeql  18650  sgrppropd  18665  ismndd  18690  mndpropd  18693  mndpsuppss  18699  mhmeql  18760  mndind  18762  frmdup3lem  18800  mhmmnd  19003  issubg4  19084  ssnmz  19105  f1otrspeq  19384  psgneu  19443  sylow2blem3  19559  lsmdisj2  19619  pj1eu  19633  efgredlem  19684  frgpuplem  19709  frgpnabl  19812  dmdprdsplitlem  19976  pgpfac1lem3  20016  pgpfaclem3  20022  ablsimpgcygd  20045  rngpropd  20090  ringpropd  20204  dvdsrtr  20284  rngcinv  20553  ringcinv  20587  islmhm2  20952  lmhmpropd  20987  prmirredlem  21389  psgndiflemA  21517  lsmcss  21608  dsmmlss  21660  uvcf1  21708  frlmup1  21714  assapropd  21788  evlslem1  21996  coe1tmmul2  22169  mamucl  22295  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  mamulid  22335  mamurid  22336  dmatsubcl  22392  dmatmulcl  22394  mdetunilem7  22512  mdetunilem9  22514  cramer0  22584  cpmatmcllem  22612  mat2pmatf1  22623  decpmatmul  22666  pmatcollpw1  22670  pm2mpf1lem  22688  pm2mpmhmlem2  22713  chpidmat  22741  cpmadugsumlemB  22768  cpmadugsumlemC  22769  toponmre  22987  restbas  23052  iscncl  23163  cnpdis  23187  lmcnp  23198  dishaus  23276  cmpcovf  23285  hauscmplem  23300  dfconn2  23313  clsconn  23324  2ndcctbss  23349  1stccnp  23356  islly2  23378  llyidm  23382  cldllycmp  23389  locfincmp  23420  kgentopon  23432  1stckgenlem  23447  ptpjpre1  23465  ptbasfi  23475  txcls  23498  ptpjopn  23506  xkoccn  23513  txcnp  23514  txcmpb  23538  xkoptsub  23548  xkoco2cn  23552  xkoinjcn  23581  qtopcn  23608  qtoprest  23611  regr1lem  23633  regr1lem2  23634  kqreglem1  23635  qtophmeo  23711  fgabs  23773  hauspwpwf1  23881  flimfnfcls  23922  fclscmp  23924  cnpfcf  23935  ptcmplem4  23949  ptcmplem5  23950  cnextfval  23956  cnextfun  23958  tmdgsum2  23990  tsmsval2  24024  utoptop  24129  utop3cls  24146  ismet2  24228  blin  24316  metss2lem  24406  methaus  24415  met1stc  24416  met2ndci  24417  metcnp  24436  metcnpi3  24441  metustto  24448  metustfbas  24452  nlmvscn  24582  nrginvrcn  24587  nghmcn  24640  xrsxmet  24705  reconnlem1  24722  reconn  24724  xrge0tsms  24730  xmetdcn2  24733  metdscn  24752  addcnlem  24760  mulc1cncf  24805  cncfco  24807  cnheiborlem  24860  cnheibor  24861  nmoleub2lem2  25023  ipcn  25153  iscfil3  25180  cfilfcls  25181  iscmet3  25200  caubl  25215  bcthlem5  25235  rrxdstprj1  25316  minveclem3b  25335  minveclem7  25342  pmltpc  25358  ovolshftlem1  25417  ovolscalem1  25421  ioombl1  25470  uniioombllem6  25496  dyadss  25502  dyaddisjlem  25503  dyadmax  25506  opnmbllem  25509  itg1addlem2  25605  itg2seq  25650  bddmulibl  25747  limcfval  25780  ellimc3  25787  limciun  25802  dveflem  25890  rolle  25901  dvlip2  25907  c1liplem1  25908  dvgt0lem1  25914  dvgt0  25916  dvlt0  25917  dvne0  25923  dvcnvre  25931  dvfsumrlimge0  25944  ftc1lem6  25955  itgsubst  25963  mdegmullem  25990  ply1domn  26036  fta1g  26082  fta1b  26084  dgrlem  26141  coeid  26150  plydivalg  26214  aannenlem1  26243  aalioulem6  26252  ulmcn  26315  mtestbdd  26321  abelthlem8  26356  efif1olem4  26461  chordthm  26754  xrlimcnp  26885  lgamgulmlem5  26950  isppw2  27032  fsumvma2  27132  perfectlem2  27148  lgsdilem  27242  lgsquad2lem2  27303  lgsquad3  27305  2sqlem5  27340  2sqlem9  27345  rpvmasumlem  27405  dchrisum0flb  27428  pntpbnd  27506  pntibndlem3  27510  pntlem3  27527  pntleml  27529  nosupbday  27624  noinfbday  27639  noetasuplem4  27655  noetainflem4  27659  noetalem1  27660  slerec  27738  madebdaylemlrcut  27817  bdayon  28180  n0sfincut  28253  eucliddivs  28272  remulscllem2  28359  tgjustc1  28409  tgjustc2  28410  tgbtwnconn1lem3  28508  legtrid  28525  tglinethru  28570  tglnpt2  28575  tglineintmo  28576  mirreu3  28588  perpcom  28647  footexALT  28652  footex  28655  mideu  28672  opphllem1  28681  lnopp2hpgb  28697  axsegcon  28861  axpasch  28875  axeuclidlem  28896  ecgrtg  28917  elntg  28918  eengtrkg  28920  upgr1eopALT  29051  usgredg4  29151  usgr1eop  29184  usgr1v  29190  subuhgr  29220  subumgr  29222  subusgr  29223  nbuhgr2vtx1edgb  29286  wwlksnext  29830  usgr2wspthon  29902  clwlkclwwlkf1  29946  clwwisshclwwslem  29950  n4cyclfrgr  30227  dlwwlknondlwlknonf1o  30301  vacn  30630  ubthlem1  30806  ubthlem3  30808  minvecolem7  30819  chocunii  31237  pjhthmo  31238  pjhthlem2  31328  nmopub2tALT  31845  nmfnleub2  31862  kbass5  32056  mdslmd1lem1  32261  mdslmd1lem2  32262  mdsymlem5  32343  fcobij  32652  xrofsup  32697  mgcf1o  32936  xrge0tsmsd  33009  symgcntz  33049  archiabllem2a  33155  gsumvsca1  33186  gsumvsca2  33187  isarchiofld  33302  prmidl2  33419  ssmxidl  33452  constrelextdg2  33744  smatrcl  33793  reff  33836  ordtconnlem1  33921  qqhval2  33979  esumpcvgval  34075  imambfm  34260  ballotlemsf1o  34512  signstfvneq0  34570  pconnconn  35225  connpconn  35229  cvmliftmo  35278  cvmlift2lem10  35306  cvmlift2lem12  35308  cvmlift3lem7  35319  mrsubff1  35508  msubff1  35550  ifscgr  36039  cgrxfr  36050  btwnconn1lem13  36094  ellines  36147  weiunso  36461  weiunfr  36462  unblimceq0lem  36501  unbdqndv2  36506  irrdiff  37321  matunitlindflem1  37617  poimirlem4  37625  poimirlem13  37634  poimirlem14  37635  heicant  37656  opnmbllem0  37657  mblfinlem3  37660  itg2addnclem  37672  itg2addnc  37675  ftc1cnnc  37693  sstotbnd  37776  cntotbnd  37797  ismtyima  37804  heibor1lem  37810  heiborlem10  37821  bfp  37825  rrncmslem  37833  islshpsm  38980  lsatcmp  39003  islshpat  39017  lfl0f  39069  iscvlat2N  39324  ishlat3N  39354  3dim1  39468  islvol5  39580  lvoli2  39582  lncvrelatN  39782  lncmp  39784  paddasslem10  39830  pclfinclN  39951  pexmidlem8N  39978  idltrn  40151  cdleme42keg  40487  cdleme42mgN  40489  cdlemf2  40563  cdlemg2cex  40592  trlcoat  40724  tendoex  40976  erngdvlem4  40992  erngdvlem4-rN  41000  dialss  41047  dibglbN  41167  diblss  41171  dihlsscpre  41235  dihglblem2aN  41294  dihglblem4  41298  dihglblem5  41299  dih1dimatlem  41330  dihglblem6  41341  lcfl7N  41502  lcfrlem9  41551  mapdh9a  41790  hdmapglem7  41930  aks4d1p8  42082  isprimroot  42088  evl1gprodd  42112  hashnexinjle  42124  deg1gprod  42135  sticksstones22  42163  grpods  42189  renegeulemv  42363  sn-subeu  42422  remulinvcom  42428  imacrhmcl  42509  fidomncyc  42530  fsuppind  42585  prjspertr  42600  prjspreln0  42604  flt4lem7  42654  nna4b4nsq  42655  isnacs3  42705  nacsfix  42707  mzpsubst  42743  eldioph2lem2  42756  eldioph2  42757  eldioph2b  42758  diophin  42767  diophun  42768  rencldnfilem  42815  irrapxlem3  42819  irrapxlem5  42821  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell1qrge1  42865  pell1qrgaplem  42868  monotuz  42937  monotoddzzfi  42938  acongtr  42974  acongrep  42976  jm2.26a  42996  jm2.26lem3  42997  jm2.26  42998  jm2.27b  43002  jm2.27  43004  wepwsolem  43038  fnwe2lem2  43047  hbtlem5  43124  hbt  43126  mpaaeu  43146  cantnftermord  43316  cantnfresb  43320  omabs2  43328  tfsconcatun  43333  tfsconcatfn  43334  tfsconcatfv1  43335  tfsconcatfv2  43336  tfsconcatfv  43337  tfsconcatrn  43338  naddcnff  43358  oaun3lem1  43370  rfovcnvf1od  44000  mnurndlem1  44277  fnchoice  45030  rfcnnnub  45037  disjxp1  45070  ioondisj2  45498  iccintsng  45528  fprodcn  45605  lptioo2  45636  lptioo1  45637  limclner  45656  dvdsn1add  45944  stoweidlem14  46019  stoweidlem27  46032  stoweidlem34  46039  stoweidlem49  46054  stoweidlem56  46061  fourierdlem87  46198  iundjiun  46465  ismeannd  46472  hoidmvle  46605  prproropf1olem2  47509  perfectALTVlem2  47727  mogoldbb  47790  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  grimgrtri  47952  isubgr3stgrlem6  47974  rngcinvALTV  48268  ringcinvALTV  48302  lindslinindsimp2lem5  48455  itscnhlinecirc02p  48778  toslat  48974  iinfssclem3  49049  iinfssc  49050  iinfsubc  49051  discsubc  49057  iinfconstbas  49059  imasubc3  49149  upciclem4  49162  natoppf  49222  tposcurf1  49292  fucofvalg  49311  fuco22  49332  fuco22natlem  49338  functhinclem4  49440  functhincfun  49442  arweuthinc  49522  lanfval  49606  ranfval  49607  islmd  49658  iscmd  49659