Theorem simplrl 786

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  disjxiun  4837  f1imass  6742  f1prex  6760  soisoi  6799  riota5f  6857  tfrlem9a  7715  oeeui  7916  oaabs2  7959  omabs  7961  omxpenlem  8297  fopwdom  8304  frfi  8441  marypha1lem  8575  ordiso2  8656  oismo  8681  wemaplem3  8689  cantnf  8834  isinffi  9098  dfac12lem2  9248  dfac12lem3  9249  infxp  9319  infmap2  9322  infpssrlem5  9411  fin23lem11  9421  fin23lem24  9426  fin23lem26  9429  isf32lem2  9458  isf32lem4  9460  fin1a2lem13  9516  fin1a2s  9518  ttukeylem5  9617  fpwwe2lem12  9745  fpwwe2lem13  9746  wunex2  9842  tskord  9884  prlem934  10137  mulcmpblnr  10174  dedekind  10482  addid1  10498  cnegex  10499  negeu  10553  add20  10822  divdivdiv  11008  ltmul12a  11161  lediv12a  11198  cru  11294  uzwo3  11998  xleadd1a  12297  xlemul1a  12332  ixxun  12405  ixxss12  12409  elfz0ubfz0  12663  mulexpz  13119  leexp1a  13138  expmulnbnd  13215  swrdccat3  13712  abs3lem  14297  rexanre  14305  cau3lem  14313  lo1bdd2  14474  o1lo1  14487  rlimclim1  14495  rlimclim  14496  lo1resb  14514  o1resb  14516  rlimcn2  14540  o1of2  14562  o1rlimmul  14568  lo1add  14576  lo1mul  14577  isercolllem1  14614  climcau  14620  summolem2  14666  summo  14667  o1fsum  14763  prodmolem2  14882  qredeu  15586  isprm5  15632  pclem  15756  pcqmul  15771  pcexp  15777  pcneg  15791  pcprmpw2  15799  pcadd  15806  prmpwdvds  15821  4sqlem13  15874  vdwlem2  15899  vdwlem7  15904  vdwlem11  15908  vdwlem12  15909  ramval  15925  ramz2  15941  ramcl  15946  prmgaplem6  15973  cshwshashlem2  16011  imasval  16372  imasdsval  16376  mreexexd  16509  issubc3  16709  idfucl  16741  funcres2c  16761  fucpropd  16837  xpcval  17018  prfval  17040  evlfcl  17063  curf12  17068  curf1cl  17069  curf2  17070  curfcl  17073  curfuncf  17079  curf2ndf  17088  hof2val  17097  hofcl  17100  hofpropd  17108  yonedalem4a  17116  yonedainv  17122  poslubmo  17347  posglbmo  17348  isipodrs  17362  acsmapd  17379  acsinfd  17381  ismndd  17514  mndpropd  17517  mhmeql  17565  mrcmndind  17567  frmdup3lem  17604  mhmmnd  17738  issubg4  17811  ssnmz  17834  f1otrspeq  18064  psgneu  18123  sylow2blem3  18234  lsmdisj2  18292  pj1eu  18306  efgredlem  18357  frgpuplem  18382  frgpnabl  18475  dmdprdsplitlem  18634  pgpfac1lem3  18674  pgpfaclem3  18680  ringpropd  18780  dvdsrtr  18850  islmhm2  19241  lmhmpropd  19276  assapropd  19532  evlslem1  19719  coe1tmmul2  19850  prmirredlem  20045  psgndiflemA  20151  lsmcss  20242  dsmmlss  20294  uvcf1  20337  frlmup1  20343  mamucl  20413  mamuass  20414  mamudi  20415  mamudir  20416  mamuvs1  20417  mamuvs2  20418  mamulid  20453  mamurid  20454  dmatsubcl  20511  dmatmulcl  20513  mdetunilem7  20631  mdetunilem9  20633  cramer0  20705  cpmatmcllem  20732  mat2pmatf1  20743  decpmatmul  20786  pmatcollpw1  20790  pm2mpf1lem  20808  pm2mpmhmlem2  20833  chpidmat  20861  cpmadugsumlemB  20888  cpmadugsumlemC  20889  toponmre  21107  restbas  21172  iscncl  21283  cnpdis  21307  lmcnp  21318  dishaus  21396  cmpcovf  21404  hauscmplem  21419  dfconn2  21432  clsconn  21443  2ndcctbss  21468  1stccnp  21475  islly2  21497  llyidm  21501  cldllycmp  21508  locfincmp  21539  kgentopon  21551  1stckgenlem  21566  ptpjpre1  21584  ptbasfi  21594  txcls  21617  ptpjopn  21625  xkoccn  21632  txcnp  21633  txcmpb  21657  xkoptsub  21667  xkoco2cn  21671  xkoinjcn  21700  qtopcn  21727  qtoprest  21730  regr1lem  21752  regr1lem2  21753  kqreglem1  21754  qtophmeo  21830  fgabs  21892  hauspwpwf1  22000  flimfnfcls  22041  fclscmp  22043  cnpfcf  22054  ptcmplem4  22068  ptcmplem5  22069  cnextfval  22075  cnextfun  22077  tmdgsum2  22109  tsmsval2  22142  utoptop  22247  utop3cls  22264  ismet2  22347  blin  22435  metss2lem  22525  methaus  22534  met1stc  22535  met2ndci  22536  metcnp  22555  metcnpi3  22560  metustto  22567  metustfbas  22571  nlmvscn  22700  nrginvrcn  22705  nghmcn  22758  xrsxmet  22821  reconnlem1  22838  reconn  22840  xrge0tsms  22846  xmetdcn2  22849  metdscn  22868  addcnlem  22876  mulc1cncf  22917  cncfco  22919  cnheiborlem  22962  cnheibor  22963  nmoleub2lem2  23124  ipcn  23253  iscfil3  23279  cfilfcls  23280  iscmet3  23299  caubl  23314  bcthlem5  23333  rrxdstprj1  23400  minveclem3b  23407  minveclem7  23414  pmltpc  23427  ovolshftlem1  23486  ovolscalem1  23490  ioombl1  23539  uniioombllem6  23565  dyadss  23571  dyaddisjlem  23572  dyadmax  23575  opnmbllem  23578  itg1addlem2  23674  itg2seq  23719  bddmulibl  23815  limcfval  23846  ellimc3  23853  limciun  23868  dveflem  23952  rolle  23963  dvlip2  23968  c1liplem1  23969  dvgt0lem1  23975  dvgt0  23977  dvlt0  23978  dvne0  23984  dvcnvre  23992  dvfsumrlimge0  24003  ftc1lem6  24014  itgsubst  24022  mdegmullem  24048  ply1domn  24093  fta1g  24137  fta1b  24139  dgrlem  24195  coeid  24204  plydivalg  24264  aannenlem1  24293  aalioulem6  24302  ulmcn  24363  mtestbdd  24369  abelthlem8  24403  efif1olem4  24502  chordthm  24774  xrlimcnp  24905  lgamgulmlem5  24969  isppw2  25051  fsumvma2  25149  perfectlem2  25165  lgsdilem  25259  lgsquad2lem2  25320  lgsquad3  25322  2sqlem5  25357  2sqlem9  25362  rpvmasumlem  25386  dchrisum0flb  25409  pntpbnd  25487  pntibndlem3  25491  pntlem3  25508  pntleml  25510  tgbtwnconn1lem3  25679  legtrid  25696  tglinethru  25741  tglnpt2  25746  tglineintmo  25747  mirreu3  25759  perpcom  25818  footex  25823  mideu  25840  opphllem1  25849  lnopp2hpgb  25865  axsegcon  26017  axpasch  26031  axeuclidlem  26052  ecgrtg  26073  elntg  26074  eengtrkg  26075  upgr1eopALT  26222  usgredg4  26320  usgr1eop  26354  usgr1v  26360  subuhgr  26390  subumgr  26392  subusgr  26393  nbuhgr2vtx1edgb  26460  wwlksnext  27026  usgr2wspthon  27103  clwwisshclwwslem  27153  n4cyclfrgr  27462  dlwwlknondlwlknonf1o  27541  vacn  27874  ubthlem1  28051  ubthlem3  28053  minvecolem7  28064  chocunii  28485  pjhthmo  28486  pjhthlem2  28576  nmopub2tALT  29093  nmfnleub2  29110  kbass5  29304  mdslmd1lem1  29509  mdslmd1lem2  29510  mdsymlem5  29591  fcobij  29824  xrofsup  29857  archiabllem2a  30070  gsumvsca1  30104  gsumvsca2  30105  xrge0tsmsd  30107  isarchiofld  30139  smatrcl  30184  reff  30228  ordtconnlem1  30292  qqhval2  30348  esumpcvgval  30462  imambfm  30646  ballotlemsf1o  30897  signstfvneq0  30971  pconnconn  31533  connpconn  31537  cvmliftmo  31586  cvmlift2lem10  31614  cvmlift2lem12  31616  cvmlift3lem7  31627  mrsubff1  31731  msubff1  31773  frpomin  32056  noprefixmo  32166  noetalem3  32183  slerec  32241  ifscgr  32469  cgrxfr  32480  btwnconn1lem13  32524  ellines  32577  unblimceq0lem  32811  unbdqndv2  32816  matunitlindflem1  33715  poimirlem4  33723  poimirlem13  33732  poimirlem14  33733  heicant  33754  opnmbllem0  33755  mblfinlem3  33758  itg2addnclem  33770  itg2addnc  33773  ftc1cnnc  33793  sstotbnd  33882  cntotbnd  33903  ismtyima  33910  heibor1lem  33916  heiborlem10  33927  bfp  33931  rrncmslem  33939  islshpsm  34757  lsatcmp  34780  islshpat  34794  lfl0f  34846  iscvlat2N  35101  ishlat3N  35131  3dim1  35244  islvol5  35356  lvoli2  35358  lncvrelatN  35558  lncmp  35560  paddasslem10  35606  pclfinclN  35727  pexmidlem8N  35754  idltrn  35927  cdleme42keg  36264  cdleme42mgN  36266  cdlemf2  36340  cdlemg2cex  36369  trlcoat  36501  tendoex  36753  erngdvlem4  36769  erngdvlem4-rN  36777  dialss  36824  dibglbN  36944  diblss  36948  dihlsscpre  37012  dihglblem2aN  37071  dihglblem4  37075  dihglblem5  37076  dih1dimatlem  37107  dihglblem6  37118  lcfl7N  37279  lcfrlem9  37328  mapdh9a  37567  hdmapglem7  37707  isnacs3  37772  nacsfix  37774  mzpsubst  37810  eldioph2lem2  37823  eldioph2  37824  eldioph2b  37825  diophin  37835  diophun  37836  rencldnfilem  37883  irrapxlem3  37887  irrapxlem5  37889  pell1234qrreccl  37917  pell1234qrmulcl  37918  pell1qrge1  37933  pell1qrgaplem  37936  monotuz  38004  monotoddzzfi  38005  rpexpmord  38011  acongtr  38043  acongrep  38045  jm2.26a  38065  jm2.26lem3  38066  jm2.26  38067  jm2.27b  38071  jm2.27  38073  wepwsolem  38110  fnwe2lem2  38119  hbtlem5  38196  hbt  38198  mpaaeu  38218  rfovcnvf1od  38795  fnchoice  39679  rfcnnnub  39686  disjxp1  39728  ioondisj2  40195  iccintsng  40227  fprodcn  40309  lptioo2  40340  lptioo1  40341  limclner  40360  dvdsn1add  40631  stoweidlem14  40707  stoweidlem27  40720  stoweidlem34  40727  stoweidlem49  40742  stoweidlem56  40749  fourierdlem87  40886  iundjiun  41153  ismeannd  41160  hoidmvle  41293  pfxccat3  41998  perfectALTVlem2  42203  mogoldbb  42245  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  mgmhmeql  42368  rngcinv  42546  rngcinvALTV  42558  ringcinv  42597  ringcinvALTV  42621  mndpsuppss  42717  lindslinindsimp2lem5  42816