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  5088  frpomin  6287  f1imass  7198  f1prex  7218  soisoi  7262  riota5f  7331  frxp3  8081  xpord3pred  8082  tfrlem9a  8305  oeeui  8517  oaabs2  8564  omabs  8566  naddssim  8600  omxpenlem  8991  fopwdom  8998  frfi  9169  marypha1lem  9317  ordiso2  9401  oismo  9426  wemaplem3  9434  cantnf  9583  ttrclss  9610  isinffi  9882  dfac12lem2  10033  dfac12lem3  10034  infxp  10102  infmap2  10105  infpssrlem5  10195  fin23lem11  10205  fin23lem24  10210  fin23lem26  10213  isf32lem2  10242  isf32lem4  10244  fin1a2lem13  10300  fin1a2s  10302  ttukeylem5  10401  fpwwe2lem11  10529  fpwwe2lem12  10530  wunex2  10626  tskord  10668  prlem934  10921  mulcmpblnr  10959  dedekind  11273  addrid  11290  cnegex  11291  negeu  11347  add20  11626  divdivdiv  11819  ltmul12a  11974  lediv12a  12012  cru  12114  uzwo3  12838  xleadd1a  13149  xlemul1a  13184  ixxun  13258  ixxss12  13262  elfz0ubfz0  13529  mulexpz  14006  rpexpmord  14072  leexp1a  14079  expmulnbnd  14139  swrdccatin1  14629  pfxccatin12lem3  14636  pfxccat3  14638  abs3lem  15243  rexanre  15251  cau3lem  15259  lo1bdd2  15428  o1lo1  15441  rlimclim1  15449  rlimclim  15450  lo1resb  15468  o1resb  15470  rlimcn3  15494  o1of2  15517  o1rlimmul  15523  lo1add  15531  lo1mul  15532  isercolllem1  15569  climcau  15575  summolem2  15620  summo  15621  o1fsum  15717  prodmolem2  15839  qredeu  16566  isprm5  16615  pclem  16747  pcqmul  16762  pcexp  16768  pcneg  16783  pcprmpw2  16791  pcadd  16798  prmpwdvds  16813  4sqlem13  16866  vdwlem2  16891  vdwlem7  16896  vdwlem11  16900  vdwlem12  16901  ramval  16917  ramz2  16933  ramcl  16938  prmgaplem6  16965  cshwshashlem2  17005  imasval  17412  imasdsval  17416  mreexexd  17551  issubc3  17753  idfucl  17785  funcres2c  17807  fucpropd  17884  xpcval  18080  prfval  18102  evlfcl  18125  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  curfuncf  18141  curf2ndf  18150  hof2val  18159  hofcl  18162  hofpropd  18170  yonedalem4a  18178  yonedainv  18184  poslubmo  18312  posglbmo  18313  isipodrs  18440  acsmapd  18457  acsinfd  18459  chnpof1  18533  mgmhmeql  18621  sgrppropd  18636  ismndd  18661  mndpropd  18664  mndpsuppss  18670  mhmeql  18731  mndind  18733  frmdup3lem  18771  mhmmnd  18974  issubg4  19055  ssnmz  19076  f1otrspeq  19357  psgneu  19416  sylow2blem3  19532  lsmdisj2  19592  pj1eu  19606  efgredlem  19657  frgpuplem  19682  frgpnabl  19785  dmdprdsplitlem  19949  pgpfac1lem3  19989  pgpfaclem3  19995  ablsimpgcygd  20018  rngpropd  20090  ringpropd  20204  dvdsrtr  20284  rngcinv  20550  ringcinv  20584  islmhm2  20970  lmhmpropd  21005  prmirredlem  21407  psgndiflemA  21536  lsmcss  21627  dsmmlss  21679  uvcf1  21727  frlmup1  21733  assapropd  21807  evlslem1  22015  coe1tmmul2  22188  mamucl  22314  mamuass  22315  mamudi  22316  mamudir  22317  mamuvs1  22318  mamuvs2  22319  mamulid  22354  mamurid  22355  dmatsubcl  22411  dmatmulcl  22413  mdetunilem7  22531  mdetunilem9  22533  cramer0  22603  cpmatmcllem  22631  mat2pmatf1  22642  decpmatmul  22685  pmatcollpw1  22689  pm2mpf1lem  22707  pm2mpmhmlem2  22732  chpidmat  22760  cpmadugsumlemB  22787  cpmadugsumlemC  22788  toponmre  23006  restbas  23071  iscncl  23182  cnpdis  23206  lmcnp  23217  dishaus  23295  cmpcovf  23304  hauscmplem  23319  dfconn2  23332  clsconn  23343  2ndcctbss  23368  1stccnp  23375  islly2  23397  llyidm  23401  cldllycmp  23408  locfincmp  23439  kgentopon  23451  1stckgenlem  23466  ptpjpre1  23484  ptbasfi  23494  txcls  23517  ptpjopn  23525  xkoccn  23532  txcnp  23533  txcmpb  23557  xkoptsub  23567  xkoco2cn  23571  xkoinjcn  23600  qtopcn  23627  qtoprest  23630  regr1lem  23652  regr1lem2  23653  kqreglem1  23654  qtophmeo  23730  fgabs  23792  hauspwpwf1  23900  flimfnfcls  23941  fclscmp  23943  cnpfcf  23954  ptcmplem4  23968  ptcmplem5  23969  cnextfval  23975  cnextfun  23977  tmdgsum2  24009  tsmsval2  24043  utoptop  24147  utop3cls  24164  ismet2  24246  blin  24334  metss2lem  24424  methaus  24433  met1stc  24434  met2ndci  24435  metcnp  24454  metcnpi3  24459  metustto  24466  metustfbas  24470  nlmvscn  24600  nrginvrcn  24605  nghmcn  24658  xrsxmet  24723  reconnlem1  24740  reconn  24742  xrge0tsms  24748  xmetdcn2  24751  metdscn  24770  addcnlem  24778  mulc1cncf  24823  cncfco  24825  cnheiborlem  24878  cnheibor  24879  nmoleub2lem2  25041  ipcn  25171  iscfil3  25198  cfilfcls  25199  iscmet3  25218  caubl  25233  bcthlem5  25253  rrxdstprj1  25334  minveclem3b  25353  minveclem7  25360  pmltpc  25376  ovolshftlem1  25435  ovolscalem1  25439  ioombl1  25488  uniioombllem6  25514  dyadss  25520  dyaddisjlem  25521  dyadmax  25524  opnmbllem  25527  itg1addlem2  25623  itg2seq  25668  bddmulibl  25765  limcfval  25798  ellimc3  25805  limciun  25820  dveflem  25908  rolle  25919  dvlip2  25925  c1liplem1  25926  dvgt0lem1  25932  dvgt0  25934  dvlt0  25935  dvne0  25941  dvcnvre  25949  dvfsumrlimge0  25962  ftc1lem6  25973  itgsubst  25981  mdegmullem  26008  ply1domn  26054  fta1g  26100  fta1b  26102  dgrlem  26159  coeid  26168  plydivalg  26232  aannenlem1  26261  aalioulem6  26270  ulmcn  26333  mtestbdd  26339  abelthlem8  26374  efif1olem4  26479  chordthm  26772  xrlimcnp  26903  lgamgulmlem5  26968  isppw2  27050  fsumvma2  27150  perfectlem2  27166  lgsdilem  27260  lgsquad2lem2  27321  lgsquad3  27323  2sqlem5  27358  2sqlem9  27363  rpvmasumlem  27423  dchrisum0flb  27446  pntpbnd  27524  pntibndlem3  27528  pntlem3  27545  pntleml  27547  nosupbday  27642  noinfbday  27657  noetasuplem4  27673  noetainflem4  27677  noetalem1  27678  slerec  27758  madebdaylemlrcut  27842  bdayon  28207  n0sfincut  28280  eucliddivs  28299  remulscllem2  28401  tgjustc1  28451  tgjustc2  28452  tgbtwnconn1lem3  28550  legtrid  28567  tglinethru  28612  tglnpt2  28617  tglineintmo  28618  mirreu3  28630  perpcom  28689  footexALT  28694  footex  28697  mideu  28714  opphllem1  28723  lnopp2hpgb  28739  axsegcon  28903  axpasch  28917  axeuclidlem  28938  ecgrtg  28959  elntg  28960  eengtrkg  28962  upgr1eopALT  29093  usgredg4  29193  usgr1eop  29226  usgr1v  29232  subuhgr  29262  subumgr  29264  subusgr  29265  nbuhgr2vtx1edgb  29328  wwlksnext  29869  usgr2wspthon  29941  clwlkclwwlkf1  29985  clwwisshclwwslem  29989  n4cyclfrgr  30266  dlwwlknondlwlknonf1o  30340  vacn  30669  ubthlem1  30845  ubthlem3  30847  minvecolem7  30858  chocunii  31276  pjhthmo  31277  pjhthlem2  31367  nmopub2tALT  31884  nmfnleub2  31901  kbass5  32095  mdslmd1lem1  32300  mdslmd1lem2  32301  mdsymlem5  32382  fcobij  32698  xrofsup  32745  mgcf1o  32979  xrge0tsmsd  33037  symgcntz  33049  archiabllem2a  33158  isarchiofld  33163  gsumvsca1  33190  gsumvsca2  33191  prmidl2  33401  ssmxidl  33434  mplvrpmrhm  33572  constrelextdg2  33755  smatrcl  33804  reff  33847  ordtconnlem1  33932  qqhval2  33990  esumpcvgval  34086  imambfm  34270  ballotlemsf1o  34522  signstfvneq0  34580  pconnconn  35263  connpconn  35267  cvmliftmo  35316  cvmlift2lem10  35344  cvmlift2lem12  35346  cvmlift3lem7  35357  mrsubff1  35546  msubff1  35588  ifscgr  36077  cgrxfr  36088  btwnconn1lem13  36132  ellines  36185  weiunso  36499  weiunfr  36500  unblimceq0lem  36539  unbdqndv2  36544  irrdiff  37359  matunitlindflem1  37655  poimirlem4  37663  poimirlem13  37672  poimirlem14  37673  heicant  37694  opnmbllem0  37695  mblfinlem3  37698  itg2addnclem  37710  itg2addnc  37713  ftc1cnnc  37731  sstotbnd  37814  cntotbnd  37835  ismtyima  37842  heibor1lem  37848  heiborlem10  37859  bfp  37863  rrncmslem  37871  islshpsm  39018  lsatcmp  39041  islshpat  39055  lfl0f  39107  iscvlat2N  39362  ishlat3N  39392  3dim1  39505  islvol5  39617  lvoli2  39619  lncvrelatN  39819  lncmp  39821  paddasslem10  39867  pclfinclN  39988  pexmidlem8N  40015  idltrn  40188  cdleme42keg  40524  cdleme42mgN  40526  cdlemf2  40600  cdlemg2cex  40629  trlcoat  40761  tendoex  41013  erngdvlem4  41029  erngdvlem4-rN  41037  dialss  41084  dibglbN  41204  diblss  41208  dihlsscpre  41272  dihglblem2aN  41331  dihglblem4  41335  dihglblem5  41336  dih1dimatlem  41367  dihglblem6  41378  lcfl7N  41539  lcfrlem9  41588  mapdh9a  41827  hdmapglem7  41967  aks4d1p8  42119  isprimroot  42125  evl1gprodd  42149  hashnexinjle  42161  deg1gprod  42172  sticksstones22  42200  grpods  42226  renegeulemv  42400  sn-subeu  42459  remulinvcom  42465  imacrhmcl  42546  fidomncyc  42567  fsuppind  42622  prjspertr  42637  prjspreln0  42641  flt4lem7  42691  nna4b4nsq  42692  isnacs3  42742  nacsfix  42744  mzpsubst  42780  eldioph2lem2  42793  eldioph2  42794  eldioph2b  42795  diophin  42804  diophun  42805  rencldnfilem  42852  irrapxlem3  42856  irrapxlem5  42858  pell1234qrreccl  42886  pell1234qrmulcl  42887  pell1qrge1  42902  pell1qrgaplem  42905  monotuz  42973  monotoddzzfi  42974  acongtr  43010  acongrep  43012  jm2.26a  43032  jm2.26lem3  43033  jm2.26  43034  jm2.27b  43038  jm2.27  43040  wepwsolem  43074  fnwe2lem2  43083  hbtlem5  43160  hbt  43162  mpaaeu  43182  cantnftermord  43352  cantnfresb  43356  omabs2  43364  tfsconcatun  43369  tfsconcatfn  43370  tfsconcatfv1  43371  tfsconcatfv2  43372  tfsconcatfv  43373  tfsconcatrn  43374  naddcnff  43394  oaun3lem1  43406  rfovcnvf1od  44036  mnurndlem1  44313  fnchoice  45065  rfcnnnub  45072  disjxp1  45105  ioondisj2  45532  iccintsng  45562  fprodcn  45639  lptioo2  45670  lptioo1  45671  limclner  45688  dvdsn1add  45976  stoweidlem14  46051  stoweidlem27  46064  stoweidlem34  46071  stoweidlem49  46086  stoweidlem56  46093  fourierdlem87  46230  iundjiun  46497  ismeannd  46504  hoidmvle  46637  prproropf1olem2  47534  perfectALTVlem2  47752  mogoldbb  47815  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  grimgrtri  47979  isubgr3stgrlem6  48001  rngcinvALTV  48306  ringcinvALTV  48340  lindslinindsimp2lem5  48493  itscnhlinecirc02p  48816  toslat  49012  iinfssclem3  49087  iinfssc  49088  iinfsubc  49089  discsubc  49095  iinfconstbas  49097  imasubc3  49187  upciclem4  49200  natoppf  49260  tposcurf1  49330  fucofvalg  49349  fuco22  49370  fuco22natlem  49376  functhinclem4  49478  functhincfun  49480  arweuthinc  49560  lanfval  49644  ranfval  49645  islmd  49696  iscmd  49697