Theorem simplrl 764

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  disjxiun  4922  f1imass  6845  f1prex  6863  soisoi  6902  riota5f  6960  tfrlem9a  7824  oeeui  8027  oaabs2  8070  omabs  8072  omxpenlem  8412  fopwdom  8419  frfi  8556  marypha1lem  8690  ordiso2  8772  oismo  8797  wemaplem3  8805  cantnf  8948  isinffi  9213  dfac12lem2  9362  dfac12lem3  9363  infxp  9433  infmap2  9436  infpssrlem5  9525  fin23lem11  9535  fin23lem24  9540  fin23lem26  9543  isf32lem2  9572  isf32lem4  9574  fin1a2lem13  9630  fin1a2s  9632  ttukeylem5  9731  fpwwe2lem12  9859  fpwwe2lem13  9860  wunex2  9956  tskord  9998  prlem934  10251  mulcmpblnr  10289  dedekind  10601  addid1  10618  cnegex  10619  negeu  10674  add20  10951  divdivdiv  11140  ltmul12a  11295  lediv12a  11332  cru  11429  uzwo3  12155  xleadd1a  12460  xlemul1a  12495  ixxun  12568  ixxss12  12572  elfz0ubfz0  12825  mulexpz  13282  rpexpmord  13345  leexp1a  13352  expmulnbnd  13409  pfxccat3  13934  swrdccat3OLD  13935  abs3lem  14557  rexanre  14565  cau3lem  14573  lo1bdd2  14740  o1lo1  14753  rlimclim1  14761  rlimclim  14762  lo1resb  14780  o1resb  14782  rlimcn2  14806  o1of2  14828  o1rlimmul  14834  lo1add  14842  lo1mul  14843  isercolllem1  14880  climcau  14886  summolem2  14931  summo  14932  o1fsum  15026  prodmolem2  15147  qredeu  15856  isprm5  15905  pclem  16029  pcqmul  16044  pcexp  16050  pcneg  16064  pcprmpw2  16072  pcadd  16079  prmpwdvds  16094  4sqlem13  16147  vdwlem2  16172  vdwlem7  16177  vdwlem11  16181  vdwlem12  16182  ramval  16198  ramz2  16214  ramcl  16219  prmgaplem6  16246  cshwshashlem2  16284  imasval  16638  imasdsval  16642  mreexexd  16789  issubc3  16989  idfucl  17021  funcres2c  17041  fucpropd  17117  xpcval  17297  prfval  17319  evlfcl  17342  curf12  17347  curf1cl  17348  curf2  17349  curfcl  17352  curfuncf  17358  curf2ndf  17367  hof2val  17376  hofcl  17379  hofpropd  17387  yonedalem4a  17395  yonedainv  17401  poslubmo  17626  posglbmo  17627  isipodrs  17641  acsmapd  17658  acsinfd  17660  ismndd  17793  mndpropd  17796  mhmeql  17844  mndind  17846  frmdup3lem  17884  mhmmnd  18020  issubg4  18094  ssnmz  18117  f1otrspeq  18348  psgneu  18408  sylow2blem3  18520  lsmdisj2  18578  pj1eu  18592  efgredlem  18644  efgredlemOLD  18645  frgpuplem  18670  frgpnabl  18763  dmdprdsplitlem  18921  pgpfac1lem3  18961  pgpfaclem3  18967  ringpropd  19067  dvdsrtr  19137  islmhm2  19544  lmhmpropd  19579  assapropd  19833  evlslem1  20020  coe1tmmul2  20159  prmirredlem  20354  psgndiflemA  20459  lsmcss  20550  dsmmlss  20602  uvcf1  20650  frlmup1  20656  mamucl  20726  mamuass  20727  mamudi  20728  mamudir  20729  mamuvs1  20730  mamuvs2  20731  mamulid  20766  mamurid  20767  dmatsubcl  20823  dmatmulcl  20825  mdetunilem7  20943  mdetunilem9  20945  cramer0  21015  cpmatmcllem  21042  mat2pmatf1  21053  decpmatmul  21096  pmatcollpw1  21100  pm2mpf1lem  21118  pm2mpmhmlem2  21143  chpidmat  21171  cpmadugsumlemB  21198  cpmadugsumlemC  21199  toponmre  21417  restbas  21482  iscncl  21593  cnpdis  21617  lmcnp  21628  dishaus  21706  cmpcovf  21715  hauscmplem  21730  dfconn2  21743  clsconn  21754  2ndcctbss  21779  1stccnp  21786  islly2  21808  llyidm  21812  cldllycmp  21819  locfincmp  21850  kgentopon  21862  1stckgenlem  21877  ptpjpre1  21895  ptbasfi  21905  txcls  21928  ptpjopn  21936  xkoccn  21943  txcnp  21944  txcmpb  21968  xkoptsub  21978  xkoco2cn  21982  xkoinjcn  22011  qtopcn  22038  qtoprest  22041  regr1lem  22063  regr1lem2  22064  kqreglem1  22065  qtophmeo  22141  fgabs  22203  hauspwpwf1  22311  flimfnfcls  22352  fclscmp  22354  cnpfcf  22365  ptcmplem4  22379  ptcmplem5  22380  cnextfval  22386  cnextfun  22388  tmdgsum2  22420  tsmsval2  22453  utoptop  22558  utop3cls  22575  ismet2  22658  blin  22746  metss2lem  22836  methaus  22845  met1stc  22846  met2ndci  22847  metcnp  22866  metcnpi3  22871  metustto  22878  metustfbas  22882  nlmvscn  23011  nrginvrcn  23016  nghmcn  23069  xrsxmet  23132  reconnlem1  23149  reconn  23151  xrge0tsms  23157  xmetdcn2  23160  metdscn  23179  addcnlem  23187  mulc1cncf  23228  cncfco  23230  cnheiborlem  23273  cnheibor  23274  nmoleub2lem2  23435  ipcn  23564  iscfil3  23591  cfilfcls  23592  iscmet3  23611  caubl  23626  bcthlem5  23646  rrxdstprj1  23727  minveclem3b  23746  minveclem7  23753  pmltpc  23766  ovolshftlem1  23825  ovolscalem1  23829  ioombl1  23878  uniioombllem6  23904  dyadss  23910  dyaddisjlem  23911  dyadmax  23914  opnmbllem  23917  itg1addlem2  24013  itg2seq  24058  bddmulibl  24154  limcfval  24185  ellimc3  24192  limciun  24207  dveflem  24291  rolle  24302  dvlip2  24307  c1liplem1  24308  dvgt0lem1  24314  dvgt0  24316  dvlt0  24317  dvne0  24323  dvcnvre  24331  dvfsumrlimge0  24342  ftc1lem6  24353  itgsubst  24361  mdegmullem  24387  ply1domn  24432  fta1g  24476  fta1b  24478  dgrlem  24534  coeid  24543  plydivalg  24603  aannenlem1  24632  aalioulem6  24641  ulmcn  24702  mtestbdd  24708  abelthlem8  24742  efif1olem4  24842  chordthm  25128  xrlimcnp  25260  lgamgulmlem5  25324  isppw2  25406  fsumvma2  25504  perfectlem2  25520  lgsdilem  25614  lgsquad2lem2  25675  lgsquad3  25677  2sqlem5  25712  2sqlem9  25717  rpvmasumlem  25777  dchrisum0flb  25800  pntpbnd  25878  pntibndlem3  25882  pntlem3  25899  pntleml  25901  tgjustc1  25975  tgjustc2  25976  tgbtwnconn1lem3  26074  legtrid  26091  tglinethru  26136  tglnpt2  26141  tglineintmo  26142  mirreu3  26154  perpcom  26213  footexALT  26218  footex  26221  mideu  26238  opphllem1  26247  lnopp2hpgb  26263  axsegcon  26428  axpasch  26442  axeuclidlem  26463  ecgrtg  26484  elntg  26485  eengtrkg  26487  upgr1eopALT  26617  usgredg4  26714  usgr1eop  26747  usgr1v  26753  subuhgr  26783  subumgr  26785  subusgr  26786  nbuhgr2vtx1edgb  26849  wwlksnext  27393  usgr2wspthon  27483  clwlkclwwlkf1  27536  clwwisshclwwslem  27541  n4cyclfrgr  27837  dlwwlknondlwlknonf1o  27928  dlwwlknondlwlknonf1oOLD  27929  vacn  28260  ubthlem1  28437  ubthlem3  28439  minvecolem7  28450  chocunii  28871  pjhthmo  28872  pjhthlem2  28962  nmopub2tALT  29479  nmfnleub2  29496  kbass5  29690  mdslmd1lem1  29895  mdslmd1lem2  29896  mdsymlem5  29977  fcobij  30231  xrofsup  30265  archiabllem2a  30518  gsumvsca1  30554  gsumvsca2  30555  xrge0tsmsd  30559  isarchiofld  30598  smatrcl  30732  reff  30776  ordtconnlem1  30840  qqhval2  30896  esumpcvgval  31010  imambfm  31194  ballotlemsf1o  31446  signstfvneq0  31518  pconnconn  32092  connpconn  32096  cvmliftmo  32145  cvmlift2lem10  32173  cvmlift2lem12  32175  cvmlift3lem7  32186  mrsubff1  32310  msubff1  32352  frpomin  32628  noprefixmo  32752  noetalem3  32769  slerec  32827  ifscgr  33055  cgrxfr  33066  btwnconn1lem13  33110  ellines  33163  unblimceq0lem  33394  unbdqndv2  33399  matunitlindflem1  34358  poimirlem4  34366  poimirlem13  34375  poimirlem14  34376  heicant  34397  opnmbllem0  34398  mblfinlem3  34401  itg2addnclem  34413  itg2addnc  34416  ftc1cnnc  34436  sstotbnd  34524  cntotbnd  34545  ismtyima  34552  heibor1lem  34558  heiborlem10  34569  bfp  34573  rrncmslem  34581  islshpsm  35590  lsatcmp  35613  islshpat  35627  lfl0f  35679  iscvlat2N  35934  ishlat3N  35964  3dim1  36077  islvol5  36189  lvoli2  36191  lncvrelatN  36391  lncmp  36393  paddasslem10  36439  pclfinclN  36560  pexmidlem8N  36587  idltrn  36760  cdleme42keg  37096  cdleme42mgN  37098  cdlemf2  37172  cdlemg2cex  37201  trlcoat  37333  tendoex  37585  erngdvlem4  37601  erngdvlem4-rN  37609  dialss  37656  dibglbN  37776  diblss  37780  dihlsscpre  37844  dihglblem2aN  37903  dihglblem4  37907  dihglblem5  37908  dih1dimatlem  37939  dihglblem6  37950  lcfl7N  38111  lcfrlem9  38160  mapdh9a  38399  hdmapglem7  38539  renegeulemv  38659  prjspertr  38691  prjspreln0  38695  isnacs3  38731  nacsfix  38733  mzpsubst  38769  eldioph2lem2  38782  eldioph2  38783  eldioph2b  38784  diophin  38794  diophun  38795  rencldnfilem  38842  irrapxlem3  38846  irrapxlem5  38848  pell1234qrreccl  38876  pell1234qrmulcl  38877  pell1qrge1  38892  pell1qrgaplem  38895  monotuz  38963  monotoddzzfi  38964  acongtr  39000  acongrep  39002  jm2.26a  39022  jm2.26lem3  39023  jm2.26  39024  jm2.27b  39028  jm2.27  39030  wepwsolem  39067  fnwe2lem2  39076  hbtlem5  39153  hbt  39155  mpaaeu  39175  rfovcnvf1od  39742  mnurndlem1  40021  ablsimpgcygd  40071  fnchoice  40734  rfcnnnub  40741  disjxp1  40779  ioondisj2  41223  iccintsng  41255  fprodcn  41337  lptioo2  41368  lptioo1  41369  limclner  41388  dvdsn1add  41679  stoweidlem14  41755  stoweidlem27  41768  stoweidlem34  41775  stoweidlem49  41790  stoweidlem56  41797  fourierdlem87  41934  iundjiun  42198  ismeannd  42205  hoidmvle  42338  prproropf1olem2  43059  perfectALTVlem2  43280  mogoldbb  43343  bgoldbtbndlem2  43364  bgoldbtbndlem3  43365  mgmhmeql  43463  rngcinv  43641  rngcinvALTV  43653  ringcinv  43692  ringcinvALTV  43716  mndpsuppss  43810  lindslinindsimp2lem5  43909  itscnhlinecirc02p  44165