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 726	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  5163  frpomin  6372  f1imass  7301  f1prex  7320  soisoi  7364  riota5f  7433  frxp3  8192  xpord3pred  8193  tfrlem9a  8442  oeeui  8658  oaabs2  8705  omabs  8707  naddssim  8741  omxpenlem  9139  fopwdom  9146  frfi  9349  marypha1lem  9502  ordiso2  9584  oismo  9609  wemaplem3  9617  cantnf  9762  ttrclss  9789  isinffi  10061  dfac12lem2  10214  dfac12lem3  10215  infxp  10283  infmap2  10286  infpssrlem5  10376  fin23lem11  10386  fin23lem24  10391  fin23lem26  10394  isf32lem2  10423  isf32lem4  10425  fin1a2lem13  10481  fin1a2s  10483  ttukeylem5  10582  fpwwe2lem11  10710  fpwwe2lem12  10711  wunex2  10807  tskord  10849  prlem934  11102  mulcmpblnr  11140  dedekind  11453  addrid  11470  cnegex  11471  negeu  11526  add20  11802  divdivdiv  11995  ltmul12a  12150  lediv12a  12188  cru  12285  uzwo3  13008  xleadd1a  13315  xlemul1a  13350  ixxun  13423  ixxss12  13427  elfz0ubfz0  13689  mulexpz  14153  rpexpmord  14218  leexp1a  14225  expmulnbnd  14284  swrdccatin1  14773  pfxccatin12lem3  14780  pfxccat3  14782  abs3lem  15387  rexanre  15395  cau3lem  15403  lo1bdd2  15570  o1lo1  15583  rlimclim1  15591  rlimclim  15592  lo1resb  15610  o1resb  15612  rlimcn3  15636  o1of2  15659  o1rlimmul  15665  lo1add  15673  lo1mul  15674  isercolllem1  15713  climcau  15719  summolem2  15764  summo  15765  o1fsum  15861  prodmolem2  15983  qredeu  16705  isprm5  16754  pclem  16885  pcqmul  16900  pcexp  16906  pcneg  16921  pcprmpw2  16929  pcadd  16936  prmpwdvds  16951  4sqlem13  17004  vdwlem2  17029  vdwlem7  17034  vdwlem11  17038  vdwlem12  17039  ramval  17055  ramz2  17071  ramcl  17076  prmgaplem6  17103  cshwshashlem2  17144  imasval  17571  imasdsval  17575  mreexexd  17706  issubc3  17913  idfucl  17945  funcres2c  17968  fucpropd  18047  xpcval  18246  prfval  18268  evlfcl  18292  curf12  18297  curf1cl  18298  curf2  18299  curfcl  18302  curfuncf  18308  curf2ndf  18317  hof2val  18326  hofcl  18329  hofpropd  18337  yonedalem4a  18345  yonedainv  18351  poslubmo  18481  posglbmo  18482  isipodrs  18607  acsmapd  18624  acsinfd  18626  mgmhmeql  18754  sgrppropd  18769  ismndd  18794  mndpropd  18797  mhmeql  18861  mndind  18863  frmdup3lem  18901  mhmmnd  19104  issubg4  19185  ssnmz  19206  f1otrspeq  19489  psgneu  19548  sylow2blem3  19664  lsmdisj2  19724  pj1eu  19738  efgredlem  19789  frgpuplem  19814  frgpnabl  19917  dmdprdsplitlem  20081  pgpfac1lem3  20121  pgpfaclem3  20127  ablsimpgcygd  20150  rngpropd  20201  ringpropd  20311  dvdsrtr  20394  rngcinv  20659  ringcinv  20693  islmhm2  21060  lmhmpropd  21095  prmirredlem  21506  psgndiflemA  21642  lsmcss  21733  dsmmlss  21787  uvcf1  21835  frlmup1  21841  assapropd  21915  evlslem1  22129  coe1tmmul2  22300  mamucl  22426  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  mamulid  22468  mamurid  22469  dmatsubcl  22525  dmatmulcl  22527  mdetunilem7  22645  mdetunilem9  22647  cramer0  22717  cpmatmcllem  22745  mat2pmatf1  22756  decpmatmul  22799  pmatcollpw1  22803  pm2mpf1lem  22821  pm2mpmhmlem2  22846  chpidmat  22874  cpmadugsumlemB  22901  cpmadugsumlemC  22902  toponmre  23122  restbas  23187  iscncl  23298  cnpdis  23322  lmcnp  23333  dishaus  23411  cmpcovf  23420  hauscmplem  23435  dfconn2  23448  clsconn  23459  2ndcctbss  23484  1stccnp  23491  islly2  23513  llyidm  23517  cldllycmp  23524  locfincmp  23555  kgentopon  23567  1stckgenlem  23582  ptpjpre1  23600  ptbasfi  23610  txcls  23633  ptpjopn  23641  xkoccn  23648  txcnp  23649  txcmpb  23673  xkoptsub  23683  xkoco2cn  23687  xkoinjcn  23716  qtopcn  23743  qtoprest  23746  regr1lem  23768  regr1lem2  23769  kqreglem1  23770  qtophmeo  23846  fgabs  23908  hauspwpwf1  24016  flimfnfcls  24057  fclscmp  24059  cnpfcf  24070  ptcmplem4  24084  ptcmplem5  24085  cnextfval  24091  cnextfun  24093  tmdgsum2  24125  tsmsval2  24159  utoptop  24264  utop3cls  24281  ismet2  24364  blin  24452  metss2lem  24545  methaus  24554  met1stc  24555  met2ndci  24556  metcnp  24575  metcnpi3  24580  metustto  24587  metustfbas  24591  nlmvscn  24729  nrginvrcn  24734  nghmcn  24787  xrsxmet  24850  reconnlem1  24867  reconn  24869  xrge0tsms  24875  xmetdcn2  24878  metdscn  24897  addcnlem  24905  mulc1cncf  24950  cncfco  24952  cnheiborlem  25005  cnheibor  25006  nmoleub2lem2  25168  ipcn  25299  iscfil3  25326  cfilfcls  25327  iscmet3  25346  caubl  25361  bcthlem5  25381  rrxdstprj1  25462  minveclem3b  25481  minveclem7  25488  pmltpc  25504  ovolshftlem1  25563  ovolscalem1  25567  ioombl1  25616  uniioombllem6  25642  dyadss  25648  dyaddisjlem  25649  dyadmax  25652  opnmbllem  25655  itg1addlem2  25751  itg2seq  25797  bddmulibl  25894  limcfval  25927  ellimc3  25934  limciun  25949  dveflem  26037  rolle  26048  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  dvgt0  26063  dvlt0  26064  dvne0  26070  dvcnvre  26078  dvfsumrlimge0  26091  ftc1lem6  26102  itgsubst  26110  mdegmullem  26137  ply1domn  26183  fta1g  26229  fta1b  26231  dgrlem  26288  coeid  26297  plydivalg  26359  aannenlem1  26388  aalioulem6  26397  ulmcn  26460  mtestbdd  26466  abelthlem8  26501  efif1olem4  26605  chordthm  26898  xrlimcnp  27029  lgamgulmlem5  27094  isppw2  27176  fsumvma2  27276  perfectlem2  27292  lgsdilem  27386  lgsquad2lem2  27447  lgsquad3  27449  2sqlem5  27484  2sqlem9  27489  rpvmasumlem  27549  dchrisum0flb  27572  pntpbnd  27650  pntibndlem3  27654  pntlem3  27671  pntleml  27673  nosupbday  27768  noinfbday  27783  noetasuplem4  27799  noetainflem4  27803  noetalem1  27804  slerec  27882  madebdaylemlrcut  27955  remulscllem2  28451  tgjustc1  28501  tgjustc2  28502  tgbtwnconn1lem3  28600  legtrid  28617  tglinethru  28662  tglnpt2  28667  tglineintmo  28668  mirreu3  28680  perpcom  28739  footexALT  28744  footex  28747  mideu  28764  opphllem1  28773  lnopp2hpgb  28789  axsegcon  28960  axpasch  28974  axeuclidlem  28995  ecgrtg  29016  elntg  29017  eengtrkg  29019  upgr1eopALT  29152  usgredg4  29252  usgr1eop  29285  usgr1v  29291  subuhgr  29321  subumgr  29323  subusgr  29324  nbuhgr2vtx1edgb  29387  wwlksnext  29926  usgr2wspthon  29998  clwlkclwwlkf1  30042  clwwisshclwwslem  30046  n4cyclfrgr  30323  dlwwlknondlwlknonf1o  30397  vacn  30726  ubthlem1  30902  ubthlem3  30904  minvecolem7  30915  chocunii  31333  pjhthmo  31334  pjhthlem2  31424  nmopub2tALT  31941  nmfnleub2  31958  kbass5  32152  mdslmd1lem1  32357  mdslmd1lem2  32358  mdsymlem5  32439  fcobij  32736  xrofsup  32774  mgcf1o  32976  xrge0tsmsd  33041  symgcntz  33078  archiabllem2a  33174  gsumvsca1  33205  gsumvsca2  33206  isarchiofld  33312  prmidl2  33434  ssmxidl  33467  constrelextdg2  33737  smatrcl  33742  reff  33785  ordtconnlem1  33870  qqhval2  33928  esumpcvgval  34042  imambfm  34227  ballotlemsf1o  34478  signstfvneq0  34549  pconnconn  35199  connpconn  35203  cvmliftmo  35252  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  mrsubff1  35482  msubff1  35524  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  ellines  36116  weiunso  36432  weiunfr  36433  unblimceq0lem  36472  unbdqndv2  36477  irrdiff  37292  matunitlindflem1  37576  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  heicant  37615  opnmbllem0  37616  mblfinlem3  37619  itg2addnclem  37631  itg2addnc  37634  ftc1cnnc  37652  sstotbnd  37735  cntotbnd  37756  ismtyima  37763  heibor1lem  37769  heiborlem10  37780  bfp  37784  rrncmslem  37792  islshpsm  38936  lsatcmp  38959  islshpat  38973  lfl0f  39025  iscvlat2N  39280  ishlat3N  39310  3dim1  39424  islvol5  39536  lvoli2  39538  lncvrelatN  39738  lncmp  39740  paddasslem10  39786  pclfinclN  39907  pexmidlem8N  39934  idltrn  40107  cdleme42keg  40443  cdleme42mgN  40445  cdlemf2  40519  cdlemg2cex  40548  trlcoat  40680  tendoex  40932  erngdvlem4  40948  erngdvlem4-rN  40956  dialss  41003  dibglbN  41123  diblss  41127  dihlsscpre  41191  dihglblem2aN  41250  dihglblem4  41254  dihglblem5  41255  dih1dimatlem  41286  dihglblem6  41297  lcfl7N  41458  lcfrlem9  41507  mapdh9a  41746  hdmapglem7  41886  aks4d1p8  42044  isprimroot  42050  evl1gprodd  42074  hashnexinjle  42086  deg1gprod  42097  sticksstones22  42125  grpods  42151  renegeulemv  42344  sn-subeu  42402  remulinvcom  42408  sn-itrere  42444  sn-retire  42445  imacrhmcl  42469  fidomncyc  42490  fsuppind  42545  prjspertr  42560  prjspreln0  42564  flt4lem7  42614  nna4b4nsq  42615  isnacs3  42666  nacsfix  42668  mzpsubst  42704  eldioph2lem2  42717  eldioph2  42718  eldioph2b  42719  diophin  42728  diophun  42729  rencldnfilem  42776  irrapxlem3  42780  irrapxlem5  42782  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1qrge1  42826  pell1qrgaplem  42829  monotuz  42898  monotoddzzfi  42899  acongtr  42935  acongrep  42937  jm2.26a  42957  jm2.26lem3  42958  jm2.26  42959  jm2.27b  42963  jm2.27  42965  wepwsolem  42999  fnwe2lem2  43008  hbtlem5  43085  hbt  43087  mpaaeu  43107  cantnftermord  43282  cantnfresb  43286  omabs2  43294  tfsconcatun  43299  tfsconcatfn  43300  tfsconcatfv1  43301  tfsconcatfv2  43302  tfsconcatfv  43303  tfsconcatrn  43304  naddcnff  43324  oaun3lem1  43336  rfovcnvf1od  43966  mnurndlem1  44250  fnchoice  44929  rfcnnnub  44936  disjxp1  44971  ioondisj2  45411  iccintsng  45441  fprodcn  45521  lptioo2  45552  lptioo1  45553  limclner  45572  dvdsn1add  45860  stoweidlem14  45935  stoweidlem27  45948  stoweidlem34  45955  stoweidlem49  45970  stoweidlem56  45977  fourierdlem87  46114  iundjiun  46381  ismeannd  46388  hoidmvle  46521  prproropf1olem2  47378  perfectALTVlem2  47596  mogoldbb  47659  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  grimgrtri  47798  rngcinvALTV  47999  ringcinvALTV  48033  mndpsuppss  48096  lindslinindsimp2lem5  48191  itscnhlinecirc02p  48519  toslat  48654  functhinclem4  48711