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  5092  frpomin  6292  f1imass  7205  f1prex  7225  soisoi  7269  riota5f  7338  frxp3  8091  xpord3pred  8092  tfrlem9a  8315  oeeui  8527  oaabs2  8574  omabs  8576  naddssim  8610  omxpenlem  9002  fopwdom  9009  frfi  9190  marypha1lem  9342  ordiso2  9426  oismo  9451  wemaplem3  9459  cantnf  9608  ttrclss  9635  isinffi  9907  dfac12lem2  10058  dfac12lem3  10059  infxp  10127  infmap2  10130  infpssrlem5  10220  fin23lem11  10230  fin23lem24  10235  fin23lem26  10238  isf32lem2  10267  isf32lem4  10269  fin1a2lem13  10325  fin1a2s  10327  ttukeylem5  10426  fpwwe2lem11  10554  fpwwe2lem12  10555  wunex2  10651  tskord  10693  prlem934  10946  mulcmpblnr  10984  dedekind  11297  addrid  11314  cnegex  11315  negeu  11371  add20  11650  divdivdiv  11843  ltmul12a  11998  lediv12a  12036  cru  12138  uzwo3  12862  xleadd1a  13173  xlemul1a  13208  ixxun  13282  ixxss12  13286  elfz0ubfz0  13553  mulexpz  14027  rpexpmord  14093  leexp1a  14100  expmulnbnd  14160  swrdccatin1  14649  pfxccatin12lem3  14656  pfxccat3  14658  abs3lem  15264  rexanre  15272  cau3lem  15280  lo1bdd2  15449  o1lo1  15462  rlimclim1  15470  rlimclim  15471  lo1resb  15489  o1resb  15491  rlimcn3  15515  o1of2  15538  o1rlimmul  15544  lo1add  15552  lo1mul  15553  isercolllem1  15590  climcau  15596  summolem2  15641  summo  15642  o1fsum  15738  prodmolem2  15860  qredeu  16587  isprm5  16636  pclem  16768  pcqmul  16783  pcexp  16789  pcneg  16804  pcprmpw2  16812  pcadd  16819  prmpwdvds  16834  4sqlem13  16887  vdwlem2  16912  vdwlem7  16917  vdwlem11  16921  vdwlem12  16922  ramval  16938  ramz2  16954  ramcl  16959  prmgaplem6  16986  cshwshashlem2  17026  imasval  17433  imasdsval  17437  mreexexd  17572  issubc3  17774  idfucl  17806  funcres2c  17828  fucpropd  17905  xpcval  18101  prfval  18123  evlfcl  18146  curf12  18151  curf1cl  18152  curf2  18153  curfcl  18156  curfuncf  18162  curf2ndf  18171  hof2val  18180  hofcl  18183  hofpropd  18191  yonedalem4a  18199  yonedainv  18205  poslubmo  18333  posglbmo  18334  isipodrs  18461  acsmapd  18478  acsinfd  18480  mgmhmeql  18608  sgrppropd  18623  ismndd  18648  mndpropd  18651  mndpsuppss  18657  mhmeql  18718  mndind  18720  frmdup3lem  18758  mhmmnd  18961  issubg4  19042  ssnmz  19063  f1otrspeq  19344  psgneu  19403  sylow2blem3  19519  lsmdisj2  19579  pj1eu  19593  efgredlem  19644  frgpuplem  19669  frgpnabl  19772  dmdprdsplitlem  19936  pgpfac1lem3  19976  pgpfaclem3  19982  ablsimpgcygd  20005  rngpropd  20077  ringpropd  20191  dvdsrtr  20271  rngcinv  20540  ringcinv  20574  islmhm2  20960  lmhmpropd  20995  prmirredlem  21397  psgndiflemA  21526  lsmcss  21617  dsmmlss  21669  uvcf1  21717  frlmup1  21723  assapropd  21797  evlslem1  22005  coe1tmmul2  22178  mamucl  22304  mamuass  22305  mamudi  22306  mamudir  22307  mamuvs1  22308  mamuvs2  22309  mamulid  22344  mamurid  22345  dmatsubcl  22401  dmatmulcl  22403  mdetunilem7  22521  mdetunilem9  22523  cramer0  22593  cpmatmcllem  22621  mat2pmatf1  22632  decpmatmul  22675  pmatcollpw1  22679  pm2mpf1lem  22697  pm2mpmhmlem2  22722  chpidmat  22750  cpmadugsumlemB  22777  cpmadugsumlemC  22778  toponmre  22996  restbas  23061  iscncl  23172  cnpdis  23196  lmcnp  23207  dishaus  23285  cmpcovf  23294  hauscmplem  23309  dfconn2  23322  clsconn  23333  2ndcctbss  23358  1stccnp  23365  islly2  23387  llyidm  23391  cldllycmp  23398  locfincmp  23429  kgentopon  23441  1stckgenlem  23456  ptpjpre1  23474  ptbasfi  23484  txcls  23507  ptpjopn  23515  xkoccn  23522  txcnp  23523  txcmpb  23547  xkoptsub  23557  xkoco2cn  23561  xkoinjcn  23590  qtopcn  23617  qtoprest  23620  regr1lem  23642  regr1lem2  23643  kqreglem1  23644  qtophmeo  23720  fgabs  23782  hauspwpwf1  23890  flimfnfcls  23931  fclscmp  23933  cnpfcf  23944  ptcmplem4  23958  ptcmplem5  23959  cnextfval  23965  cnextfun  23967  tmdgsum2  23999  tsmsval2  24033  utoptop  24138  utop3cls  24155  ismet2  24237  blin  24325  metss2lem  24415  methaus  24424  met1stc  24425  met2ndci  24426  metcnp  24445  metcnpi3  24450  metustto  24457  metustfbas  24461  nlmvscn  24591  nrginvrcn  24596  nghmcn  24649  xrsxmet  24714  reconnlem1  24731  reconn  24733  xrge0tsms  24739  xmetdcn2  24742  metdscn  24761  addcnlem  24769  mulc1cncf  24814  cncfco  24816  cnheiborlem  24869  cnheibor  24870  nmoleub2lem2  25032  ipcn  25162  iscfil3  25189  cfilfcls  25190  iscmet3  25209  caubl  25224  bcthlem5  25244  rrxdstprj1  25325  minveclem3b  25344  minveclem7  25351  pmltpc  25367  ovolshftlem1  25426  ovolscalem1  25430  ioombl1  25479  uniioombllem6  25505  dyadss  25511  dyaddisjlem  25512  dyadmax  25515  opnmbllem  25518  itg1addlem2  25614  itg2seq  25659  bddmulibl  25756  limcfval  25789  ellimc3  25796  limciun  25811  dveflem  25899  rolle  25910  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  dvgt0  25925  dvlt0  25926  dvne0  25932  dvcnvre  25940  dvfsumrlimge0  25953  ftc1lem6  25964  itgsubst  25972  mdegmullem  25999  ply1domn  26045  fta1g  26091  fta1b  26093  dgrlem  26150  coeid  26159  plydivalg  26223  aannenlem1  26252  aalioulem6  26261  ulmcn  26324  mtestbdd  26330  abelthlem8  26365  efif1olem4  26470  chordthm  26763  xrlimcnp  26894  lgamgulmlem5  26959  isppw2  27041  fsumvma2  27141  perfectlem2  27157  lgsdilem  27251  lgsquad2lem2  27312  lgsquad3  27314  2sqlem5  27349  2sqlem9  27354  rpvmasumlem  27414  dchrisum0flb  27437  pntpbnd  27515  pntibndlem3  27519  pntlem3  27536  pntleml  27538  nosupbday  27633  noinfbday  27648  noetasuplem4  27664  noetainflem4  27668  noetalem1  27669  slerec  27748  madebdaylemlrcut  27831  bdayon  28196  n0sfincut  28269  eucliddivs  28288  remulscllem2  28388  tgjustc1  28438  tgjustc2  28439  tgbtwnconn1lem3  28537  legtrid  28554  tglinethru  28599  tglnpt2  28604  tglineintmo  28605  mirreu3  28617  perpcom  28676  footexALT  28681  footex  28684  mideu  28701  opphllem1  28710  lnopp2hpgb  28726  axsegcon  28890  axpasch  28904  axeuclidlem  28925  ecgrtg  28946  elntg  28947  eengtrkg  28949  upgr1eopALT  29080  usgredg4  29180  usgr1eop  29213  usgr1v  29219  subuhgr  29249  subumgr  29251  subusgr  29252  nbuhgr2vtx1edgb  29315  wwlksnext  29856  usgr2wspthon  29928  clwlkclwwlkf1  29972  clwwisshclwwslem  29976  n4cyclfrgr  30253  dlwwlknondlwlknonf1o  30327  vacn  30656  ubthlem1  30832  ubthlem3  30834  minvecolem7  30845  chocunii  31263  pjhthmo  31264  pjhthlem2  31354  nmopub2tALT  31871  nmfnleub2  31888  kbass5  32082  mdslmd1lem1  32287  mdslmd1lem2  32288  mdsymlem5  32369  fcobij  32678  xrofsup  32723  mgcf1o  32958  xrge0tsmsd  33028  symgcntz  33040  archiabllem2a  33146  isarchiofld  33151  gsumvsca1  33178  gsumvsca2  33179  prmidl2  33388  ssmxidl  33421  constrelextdg2  33713  smatrcl  33762  reff  33805  ordtconnlem1  33890  qqhval2  33948  esumpcvgval  34044  imambfm  34229  ballotlemsf1o  34481  signstfvneq0  34539  pconnconn  35203  connpconn  35207  cvmliftmo  35256  cvmlift2lem10  35284  cvmlift2lem12  35286  cvmlift3lem7  35297  mrsubff1  35486  msubff1  35528  ifscgr  36017  cgrxfr  36028  btwnconn1lem13  36072  ellines  36125  weiunso  36439  weiunfr  36440  unblimceq0lem  36479  unbdqndv2  36484  irrdiff  37299  matunitlindflem1  37595  poimirlem4  37603  poimirlem13  37612  poimirlem14  37613  heicant  37634  opnmbllem0  37635  mblfinlem3  37638  itg2addnclem  37650  itg2addnc  37653  ftc1cnnc  37671  sstotbnd  37754  cntotbnd  37775  ismtyima  37782  heibor1lem  37788  heiborlem10  37799  bfp  37803  rrncmslem  37811  islshpsm  38958  lsatcmp  38981  islshpat  38995  lfl0f  39047  iscvlat2N  39302  ishlat3N  39332  3dim1  39446  islvol5  39558  lvoli2  39560  lncvrelatN  39760  lncmp  39762  paddasslem10  39808  pclfinclN  39929  pexmidlem8N  39956  idltrn  40129  cdleme42keg  40465  cdleme42mgN  40467  cdlemf2  40541  cdlemg2cex  40570  trlcoat  40702  tendoex  40954  erngdvlem4  40970  erngdvlem4-rN  40978  dialss  41025  dibglbN  41145  diblss  41149  dihlsscpre  41213  dihglblem2aN  41272  dihglblem4  41276  dihglblem5  41277  dih1dimatlem  41308  dihglblem6  41319  lcfl7N  41480  lcfrlem9  41529  mapdh9a  41768  hdmapglem7  41908  aks4d1p8  42060  isprimroot  42066  evl1gprodd  42090  hashnexinjle  42102  deg1gprod  42113  sticksstones22  42141  grpods  42167  renegeulemv  42341  sn-subeu  42400  remulinvcom  42406  imacrhmcl  42487  fidomncyc  42508  fsuppind  42563  prjspertr  42578  prjspreln0  42582  flt4lem7  42632  nna4b4nsq  42633  isnacs3  42683  nacsfix  42685  mzpsubst  42721  eldioph2lem2  42734  eldioph2  42735  eldioph2b  42736  diophin  42745  diophun  42746  rencldnfilem  42793  irrapxlem3  42797  irrapxlem5  42799  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell1qrge1  42843  pell1qrgaplem  42846  monotuz  42914  monotoddzzfi  42915  acongtr  42951  acongrep  42953  jm2.26a  42973  jm2.26lem3  42974  jm2.26  42975  jm2.27b  42979  jm2.27  42981  wepwsolem  43015  fnwe2lem2  43024  hbtlem5  43101  hbt  43103  mpaaeu  43123  cantnftermord  43293  cantnfresb  43297  omabs2  43305  tfsconcatun  43310  tfsconcatfn  43311  tfsconcatfv1  43312  tfsconcatfv2  43313  tfsconcatfv  43314  tfsconcatrn  43315  naddcnff  43335  oaun3lem1  43347  rfovcnvf1od  43977  mnurndlem1  44254  fnchoice  45007  rfcnnnub  45014  disjxp1  45047  ioondisj2  45475  iccintsng  45505  fprodcn  45582  lptioo2  45613  lptioo1  45614  limclner  45633  dvdsn1add  45921  stoweidlem14  45996  stoweidlem27  46009  stoweidlem34  46016  stoweidlem49  46031  stoweidlem56  46038  fourierdlem87  46175  iundjiun  46442  ismeannd  46449  hoidmvle  46582  prproropf1olem2  47489  perfectALTVlem2  47707  mogoldbb  47770  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  grimgrtri  47934  isubgr3stgrlem6  47956  rngcinvALTV  48261  ringcinvALTV  48295  lindslinindsimp2lem5  48448  itscnhlinecirc02p  48771  toslat  48967  iinfssclem3  49042  iinfssc  49043  iinfsubc  49044  discsubc  49050  iinfconstbas  49052  imasubc3  49142  upciclem4  49155  natoppf  49215  tposcurf1  49285  fucofvalg  49304  fuco22  49325  fuco22natlem  49331  functhinclem4  49433  functhincfun  49435  arweuthinc  49515  lanfval  49599  ranfval  49600  islmd  49651  iscmd  49652