Theorem simplrl 788

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 487	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 739	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5102  frpomin  6331  f1imass  7252  f1prex  7272  soisoi  7316  riota5f  7385  frxp3  8135  xpord3pred  8136  tfrlem9a  8361  oeeui  8576  oaabs2  8623  omabs  8625  naddssim  8660  omxpenlem  9054  fopwdom  9061  frfi  9233  marypha1lem  9381  ordiso2  9465  oismo  9490  wemaplem3  9498  cantnf  9650  ttrclss  9677  isinffi  9966  dfac12lem2  10116  dfac12lem3  10117  infxp  10185  infmap2  10188  infpssrlem5  10279  fin23lem11  10289  fin23lem24  10294  fin23lem26  10297  isf32lem2  10326  isf32lem4  10328  fin1a2lem13  10384  fin1a2s  10386  ttukeylem5  10485  fpwwe2lem11  10614  fpwwe2lem12  10615  wunex2  10711  tskord  10753  prlem934  11006  mulcmpblnr  11044  dedekind  11361  addrid  11378  cnegex  11379  negeu  11435  add20  11714  divdivdiv  11907  ltmul12a  12062  lediv12a  12099  cru  12201  uzwo3  12958  xleadd1a  13270  xlemul1a  13305  ixxun  13379  ixxss12  13383  elfz0ubfz0  13651  mulexpz  14129  rpexpmord  14195  leexp1a  14202  expmulnbnd  14262  swrdccatin1  14752  pfxccatin12lem3  14759  pfxccat3  14761  abs3lem  15380  rexanre  15388  cau3lem  15396  lo1bdd2  15565  o1lo1  15578  rlimclim1  15586  rlimclim  15587  lo1resb  15605  o1resb  15607  rlimcn3  15631  o1of2  15654  o1rlimmul  15660  lo1add  15668  lo1mul  15669  isercolllem1  15706  climcau  15712  summolem2  15757  summo  15758  o1fsum  15855  prodmolem2  15979  qredeu  16706  isprm5  16756  pclem  16888  pcqmul  16903  pcexp  16909  pcneg  16924  pcprmpw2  16932  pcadd  16939  prmpwdvds  16954  4sqlem13  17007  vdwlem2  17032  vdwlem7  17037  vdwlem11  17041  vdwlem12  17042  ramval  17058  ramz2  17074  ramcl  17079  prmgaplem6  17106  cshwshashlem2  17146  imasval  17555  imasdsval  17559  mreexexd  17694  issubc3  17896  idfucl  17928  funcres2c  17950  fucpropd  18027  xpcval  18223  prfval  18245  evlfcl  18268  curf12  18273  curf1cl  18274  curf2  18275  curfcl  18278  curfuncf  18284  curf2ndf  18293  hof2val  18302  hofcl  18305  hofpropd  18313  yonedalem4a  18321  yonedainv  18327  poslubmo  18455  posglbmo  18456  isipodrs  18583  acsmapd  18600  acsinfd  18602  chnpof1  18676  mgmhmeql  18764  sgrppropd  18779  ismndd  18804  mndpropd  18807  mndpsuppss  18813  mhmeql  18875  mndind  18877  frmdup3lem  18915  mhmmnd  19121  issubg4  19203  ssnmz  19223  f1otrspeq  19508  psgneu  19567  sylow2blem3  19683  lsmdisj2  19743  pj1eu  19757  efgredlem  19808  frgpuplem  19833  frgpnabl  19936  dmdprdsplitlem  20100  pgpfac1lem3  20140  pgpfaclem3  20146  ablsimpgcygd  20169  rngpropd  20243  ringpropd  20362  dvdsrtr  20441  rngcinv  20713  ringcinv  20747  islmhm2  21128  lmhmpropd  21163  prmidl2  21428  prmirredlem  21582  psgndiflemA  21711  lsmcss  21802  dsmmlss  21854  uvcf1  21902  frlmup1  21908  assapropd  21981  evlslem1  22193  coe1tmmul2  22397  mamucl  22519  mamuass  22520  mamudi  22521  mamudir  22522  mamuvs1  22523  mamuvs2  22524  mamulid  22559  mamurid  22560  dmatsubcl  22616  dmatmulcl  22618  mdetunilem7  22736  mdetunilem9  22738  cramer0  22808  cpmatmcllem  22836  mat2pmatf1  22847  decpmatmul  22890  pmatcollpw1  22894  pm2mpf1lem  22912  pm2mpmhmlem2  22937  chpidmat  22965  cpmadugsumlemB  22992  cpmadugsumlemC  22993  toponmre  23211  restbas  23276  iscncl  23387  cnpdis  23411  lmcnp  23422  dishaus  23500  cmpcovf  23509  hauscmplem  23524  dfconn2  23537  clsconn  23548  2ndcctbss  23573  1stccnp  23580  islly2  23602  llyidm  23606  cldllycmp  23613  locfincmp  23644  kgentopon  23656  1stckgenlem  23671  ptpjpre1  23689  ptbasfi  23699  txcls  23722  ptpjopn  23730  xkoccn  23737  txcnp  23738  txcmpb  23762  xkoptsub  23772  xkoco2cn  23776  xkoinjcn  23805  qtopcn  23832  qtoprest  23835  regr1lem  23857  regr1lem2  23858  kqreglem1  23859  qtophmeo  23935  fgabs  23997  hauspwpwf1  24105  flimfnfcls  24146  fclscmp  24148  cnpfcf  24159  ptcmplem4  24173  ptcmplem5  24174  cnextfval  24180  cnextfun  24182  tmdgsum2  24214  tsmsval2  24248  utoptop  24352  utop3cls  24369  ismet2  24451  blin  24539  metss2lem  24629  methaus  24638  met1stc  24639  met2ndci  24640  metcnp  24659  metcnpi3  24664  metustto  24671  metustfbas  24675  nlmvscn  24805  nrginvrcn  24810  nghmcn  24863  xrsxmet  24928  reconnlem1  24945  reconn  24947  xrge0tsms  24953  xmetdcn2  24956  metdscn  24975  addcnlem  24983  mulc1cncf  25025  cncfco  25027  cnheiborlem  25074  cnheibor  25075  nmoleub2lem2  25236  ipcn  25366  iscfil3  25393  cfilfcls  25394  iscmet3  25413  caubl  25428  bcthlem5  25448  rrxdstprj1  25529  minveclem3b  25548  minveclem7  25555  pmltpc  25570  ovolshftlem1  25629  ovolscalem1  25633  ioombl1  25682  uniioombllem6  25708  dyadss  25714  dyaddisjlem  25715  dyadmax  25718  opnmbllem  25721  itg1addlem2  25817  itg2seq  25862  bddmulibl  25959  limcfval  25992  ellimc3  25999  limciun  26014  dveflem  26099  rolle  26110  dvlip2  26115  c1liplem1  26116  dvgt0lem1  26122  dvgt0  26124  dvlt0  26125  dvne0  26131  dvcnvre  26139  dvfsumrlimge0  26150  ftc1lem6  26161  itgsubst  26169  mdegmullem  26196  ply1domn  26242  fta1g  26288  fta1b  26290  dgrlem  26347  coeid  26356  plydivalg  26421  aannenlem1  26450  aalioulem6  26459  ulmcn  26520  mtestbdd  26526  abelthlem8  26560  efif1olem4  26668  chordthm  26960  xrlimcnp  27091  lgamgulmlem5  27155  isppw2  27237  fsumvma2  27336  perfectlem2  27352  lgsdilem  27446  lgsquad2lem2  27507  lgsquad3  27509  2sqlem5  27544  2sqlem9  27549  rpvmasumlem  27609  dchrisum0flb  27632  pntpbnd  27710  pntibndlem3  27714  pntlem3  27731  pntleml  27733  nosupbday  27827  noinfbday  27842  noetasuplem4  27858  noetainflem4  27862  noetalem1  27863  lesrec  27950  madebdaylemlrcut  28050  bdayons  28427  n0fincut  28506  eucliddivs  28527  bdayfinbndlem1  28618  remulscllem2  28652  tgjustc1  28702  tgjustc2  28703  tgbtwnconn1lem3  28801  legtrid  28818  tglinethru  28863  tglineintmo  28869  tglnpt2  28880  mirreu3  28885  perpcom  28944  footexALT  28949  footex  28952  mideu  28969  opphllem1  28978  lnopp2hpgb  28994  axsegcon  29186  axpasch  29200  axeuclidlem  29221  ecgrtg  29242  elntg  29243  eengtrkg  29245  upgr1eopALT  29376  usgredg4  29476  usgr1eop  29509  usgr1v  29515  subuhgr  29545  subumgr  29547  subusgr  29548  nbuhgr2vtx1edgb  29611  wwlksnext  30151  usgr2wspthon  30226  clwlkclwwlkf1  30270  clwwisshclwwslem  30274  n4cyclfrgr  30551  dlwwlknondlwlknonf1o  30625  vacn  30955  ubthlem1  31131  ubthlem3  31133  minvecolem7  31144  chocunii  31562  pjhthmo  31563  pjhthlem2  31653  nmopub2tALT  32170  nmfnleub2  32187  kbass5  32381  mdslmd1lem1  32586  mdslmd1lem2  32587  mdsymlem5  32668  fcobij  32977  xrofsup  33024  mgcf1o  33236  xrge0tsmsd  33306  symgcntz  33318  archiabllem2a  33427  isarchiofld  33432  gsumvsca1  33459  gsumvsca2  33460  ssmxidl  33674  mplvrpmrhm  33854  constrelextdg2  34054  smatrcl  34103  reff  34146  ordtconnlem1  34231  qqhval2  34289  esumpcvgval  34385  imambfm  34569  ballotlemsf1o  34821  signstfvneq0  34876  pconnconn  35594  connpconn  35598  cvmliftmo  35647  cvmlift2lem10  35675  cvmlift2lem12  35677  cvmlift3lem7  35688  mrsubff1  35877  msubff1  35919  ifscgr  36407  cgrxfr  36418  btwnconn1lem13  36462  ellines  36515  weiunso  36839  weiunfr  36840  unblimceq0lem  36957  unbdqndv2  36962  irrdiff  37830  qdiff  37831  matunitlindflem1  38127  poimirlem4  38135  poimirlem13  38144  poimirlem14  38145  heicant  38166  opnmbllem0  38167  mblfinlem3  38170  itg2addnclem  38182  itg2addnc  38185  ftc1cnnc  38203  sstotbnd  38286  cntotbnd  38307  ismtyima  38314  heibor1lem  38320  heiborlem10  38331  bfp  38335  rrncmslem  38343  islshpsm  39616  lsatcmp  39639  islshpat  39653  lfl0f  39705  iscvlat2N  39960  ishlat3N  39990  3dim1  40103  islvol5  40215  lvoli2  40217  lncvrelatN  40417  lncmp  40419  paddasslem10  40465  pclfinclN  40586  pexmidlem8N  40613  idltrn  40786  cdleme42keg  41122  cdleme42mgN  41124  cdlemf2  41198  cdlemg2cex  41227  trlcoat  41359  tendoex  41611  erngdvlem4  41627  erngdvlem4-rN  41635  dialss  41682  dibglbN  41802  diblss  41806  dihlsscpre  41870  dihglblem2aN  41929  dihglblem4  41933  dihglblem5  41934  dih1dimatlem  41965  dihglblem6  41976  lcfl7N  42137  lcfrlem9  42186  mapdh9a  42425  hdmapglem7  42565  aks4d1p8  42716  isprimroot  42722  evl1gprodd  42746  hashnexinjle  42758  deg1gprod  42769  sticksstones22  42797  grpods  42823  renegeulemv  42989  sn-subeu  43048  remulinvcom  43054  imacrhmcl  43148  fidomncyc  43165  fsuppind  43184  prjspertr  43199  prjspreln0  43203  flt4lem7  43253  nna4b4nsq  43254  isnacs3  43303  nacsfix  43305  mzpsubst  43341  eldioph2lem2  43354  eldioph2  43355  eldioph2b  43356  diophin  43365  diophun  43366  rencldnfilem  43409  irrapxlem3  43413  irrapxlem5  43415  pell1234qrreccl  43443  pell1234qrmulcl  43444  pell1qrge1  43459  pell1qrgaplem  43462  monotuz  43530  monotoddzzfi  43531  acongtr  43567  acongrep  43569  jm2.26a  43589  jm2.26lem3  43590  jm2.26  43591  jm2.27b  43595  jm2.27  43597  wepwsolem  43631  fnwe2lem2  43640  hbtlem5  43717  hbt  43719  mpaaeu  43739  cantnftermord  43909  cantnfresb  43913  omabs2  43921  tfsconcatun  43926  tfsconcatfn  43927  tfsconcatfv1  43928  tfsconcatfv2  43929  tfsconcatfv  43930  tfsconcatrn  43931  naddcnff  43951  oaun3lem1  43963  rfovcnvf1od  44592  mnurndlem1  44855  fnchoice  45607  rfcnnnub  45614  disjxp1  45647  ioondisj2  46067  iccintsng  46097  fprodcn  46174  lptioo2  46205  lptioo1  46206  limclner  46223  dvdsn1add  46511  stoweidlem14  46586  stoweidlem27  46599  stoweidlem34  46606  stoweidlem49  46621  stoweidlem56  46628  fourierdlem87  46765  iundjiun  47032  ismeannd  47039  hoidmvle  47172  prproropf1olem2  48108  nprmmul2  48132  perfectALTVlem2  48342  mogoldbb  48405  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  grimgrtri  48569  isubgr3stgrlem6  48591  rngcinvALTV  48896  ringcinvALTV  48930  lindslinindsimp2lem5  49093  itscnhlinecirc02p  49416  toslat  49611  iinfssclem3  49685  iinfssc  49686  iinfsubc  49687  discsubc  49693  iinfconstbas  49695  imasubc3  49785  upciclem4  49798  natoppf  49858  tposcurf1  49928  fucofvalg  49947  fuco22  49968  fuco22natlem  49974  functhinclem4  50076  functhincfun  50078  arweuthinc  50158  lanfval  50242  ranfval  50243  islmd  50294  iscmd  50295