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 206  df-an 396

This theorem is referenced by:  disjxiun  5139  frpomin  6340  f1imass  7268  f1prex  7287  soisoi  7330  riota5f  7399  frxp3  8150  xpord3pred  8151  tfrlem9a  8400  oeeui  8616  oaabs2  8663  omabs  8665  naddssim  8699  omxpenlem  9091  fopwdom  9098  frfi  9306  marypha1lem  9450  ordiso2  9532  oismo  9557  wemaplem3  9565  cantnf  9710  ttrclss  9737  isinffi  10009  dfac12lem2  10161  dfac12lem3  10162  infxp  10232  infmap2  10235  infpssrlem5  10324  fin23lem11  10334  fin23lem24  10339  fin23lem26  10342  isf32lem2  10371  isf32lem4  10373  fin1a2lem13  10429  fin1a2s  10431  ttukeylem5  10530  fpwwe2lem11  10658  fpwwe2lem12  10659  wunex2  10755  tskord  10797  prlem934  11050  mulcmpblnr  11088  dedekind  11401  addrid  11418  cnegex  11419  negeu  11474  add20  11750  divdivdiv  11939  ltmul12a  12094  lediv12a  12131  cru  12228  uzwo3  12951  xleadd1a  13258  xlemul1a  13293  ixxun  13366  ixxss12  13370  elfz0ubfz0  13631  mulexpz  14093  rpexpmord  14158  leexp1a  14165  expmulnbnd  14223  swrdccatin1  14701  pfxccatin12lem3  14708  pfxccat3  14710  abs3lem  15311  rexanre  15319  cau3lem  15327  lo1bdd2  15494  o1lo1  15507  rlimclim1  15515  rlimclim  15516  lo1resb  15534  o1resb  15536  rlimcn3  15560  o1of2  15583  o1rlimmul  15589  lo1add  15597  lo1mul  15598  isercolllem1  15637  climcau  15643  summolem2  15688  summo  15689  o1fsum  15785  prodmolem2  15905  qredeu  16622  isprm5  16671  pclem  16800  pcqmul  16815  pcexp  16821  pcneg  16836  pcprmpw2  16844  pcadd  16851  prmpwdvds  16866  4sqlem13  16919  vdwlem2  16944  vdwlem7  16949  vdwlem11  16953  vdwlem12  16954  ramval  16970  ramz2  16986  ramcl  16991  prmgaplem6  17018  cshwshashlem2  17059  imasval  17486  imasdsval  17490  mreexexd  17621  issubc3  17828  idfucl  17860  funcres2c  17883  fucpropd  17962  xpcval  18161  prfval  18183  evlfcl  18207  curf12  18212  curf1cl  18213  curf2  18214  curfcl  18217  curfuncf  18223  curf2ndf  18232  hof2val  18241  hofcl  18244  hofpropd  18252  yonedalem4a  18260  yonedainv  18266  poslubmo  18396  posglbmo  18397  isipodrs  18522  acsmapd  18539  acsinfd  18541  mgmhmeql  18669  sgrppropd  18684  ismndd  18709  mndpropd  18712  mhmeql  18771  mndind  18773  frmdup3lem  18811  mhmmnd  19013  issubg4  19093  ssnmz  19114  f1otrspeq  19395  psgneu  19454  sylow2blem3  19570  lsmdisj2  19630  pj1eu  19644  efgredlem  19695  frgpuplem  19720  frgpnabl  19823  dmdprdsplitlem  19987  pgpfac1lem3  20027  pgpfaclem3  20033  ablsimpgcygd  20056  rngpropd  20107  ringpropd  20217  dvdsrtr  20300  rngcinv  20563  ringcinv  20597  islmhm2  20916  lmhmpropd  20951  prmirredlem  21391  psgndiflemA  21526  lsmcss  21617  dsmmlss  21671  uvcf1  21719  frlmup1  21725  assapropd  21798  evlslem1  22021  coe1tmmul2  22188  mamucl  22294  mamuass  22295  mamudi  22296  mamudir  22297  mamuvs1  22298  mamuvs2  22299  mamulid  22336  mamurid  22337  dmatsubcl  22393  dmatmulcl  22395  mdetunilem7  22513  mdetunilem9  22515  cramer0  22585  cpmatmcllem  22613  mat2pmatf1  22624  decpmatmul  22667  pmatcollpw1  22671  pm2mpf1lem  22689  pm2mpmhmlem2  22714  chpidmat  22742  cpmadugsumlemB  22769  cpmadugsumlemC  22770  toponmre  22990  restbas  23055  iscncl  23166  cnpdis  23190  lmcnp  23201  dishaus  23279  cmpcovf  23288  hauscmplem  23303  dfconn2  23316  clsconn  23327  2ndcctbss  23352  1stccnp  23359  islly2  23381  llyidm  23385  cldllycmp  23392  locfincmp  23423  kgentopon  23435  1stckgenlem  23450  ptpjpre1  23468  ptbasfi  23478  txcls  23501  ptpjopn  23509  xkoccn  23516  txcnp  23517  txcmpb  23541  xkoptsub  23551  xkoco2cn  23555  xkoinjcn  23584  qtopcn  23611  qtoprest  23614  regr1lem  23636  regr1lem2  23637  kqreglem1  23638  qtophmeo  23714  fgabs  23776  hauspwpwf1  23884  flimfnfcls  23925  fclscmp  23927  cnpfcf  23938  ptcmplem4  23952  ptcmplem5  23953  cnextfval  23959  cnextfun  23961  tmdgsum2  23993  tsmsval2  24027  utoptop  24132  utop3cls  24149  ismet2  24232  blin  24320  metss2lem  24413  methaus  24422  met1stc  24423  met2ndci  24424  metcnp  24443  metcnpi3  24448  metustto  24455  metustfbas  24459  nlmvscn  24597  nrginvrcn  24602  nghmcn  24655  xrsxmet  24718  reconnlem1  24735  reconn  24737  xrge0tsms  24743  xmetdcn2  24746  metdscn  24765  addcnlem  24773  mulc1cncf  24818  cncfco  24820  cnheiborlem  24873  cnheibor  24874  nmoleub2lem2  25036  ipcn  25167  iscfil3  25194  cfilfcls  25195  iscmet3  25214  caubl  25229  bcthlem5  25249  rrxdstprj1  25330  minveclem3b  25349  minveclem7  25356  pmltpc  25372  ovolshftlem1  25431  ovolscalem1  25435  ioombl1  25484  uniioombllem6  25510  dyadss  25516  dyaddisjlem  25517  dyadmax  25520  opnmbllem  25523  itg1addlem2  25619  itg2seq  25665  bddmulibl  25761  limcfval  25794  ellimc3  25801  limciun  25816  dveflem  25904  rolle  25915  dvlip2  25921  c1liplem1  25922  dvgt0lem1  25928  dvgt0  25930  dvlt0  25931  dvne0  25937  dvcnvre  25945  dvfsumrlimge0  25958  ftc1lem6  25969  itgsubst  25977  mdegmullem  26007  ply1domn  26052  fta1g  26097  fta1b  26099  dgrlem  26156  coeid  26165  plydivalg  26227  aannenlem1  26256  aalioulem6  26265  ulmcn  26328  mtestbdd  26334  abelthlem8  26369  efif1olem4  26472  chordthm  26762  xrlimcnp  26893  lgamgulmlem5  26958  isppw2  27040  fsumvma2  27140  perfectlem2  27156  lgsdilem  27250  lgsquad2lem2  27311  lgsquad3  27313  2sqlem5  27348  2sqlem9  27353  rpvmasumlem  27413  dchrisum0flb  27436  pntpbnd  27514  pntibndlem3  27518  pntlem3  27535  pntleml  27537  nosupbday  27631  noinfbday  27646  noetasuplem4  27662  noetainflem4  27666  noetalem1  27667  slerec  27745  madebdaylemlrcut  27818  remulscllem2  28222  tgjustc1  28272  tgjustc2  28273  tgbtwnconn1lem3  28371  legtrid  28388  tglinethru  28433  tglnpt2  28438  tglineintmo  28439  mirreu3  28451  perpcom  28510  footexALT  28515  footex  28518  mideu  28535  opphllem1  28544  lnopp2hpgb  28560  axsegcon  28731  axpasch  28745  axeuclidlem  28766  ecgrtg  28787  elntg  28788  eengtrkg  28790  upgr1eopALT  28923  usgredg4  29023  usgr1eop  29056  usgr1v  29062  subuhgr  29092  subumgr  29094  subusgr  29095  nbuhgr2vtx1edgb  29158  wwlksnext  29697  usgr2wspthon  29769  clwlkclwwlkf1  29813  clwwisshclwwslem  29817  n4cyclfrgr  30094  dlwwlknondlwlknonf1o  30168  vacn  30497  ubthlem1  30673  ubthlem3  30675  minvecolem7  30686  chocunii  31104  pjhthmo  31105  pjhthlem2  31195  nmopub2tALT  31712  nmfnleub2  31729  kbass5  31923  mdslmd1lem1  32128  mdslmd1lem2  32129  mdsymlem5  32210  fcobij  32498  xrofsup  32531  mgcf1o  32724  xrge0tsmsd  32765  symgcntz  32802  archiabllem2a  32896  gsumvsca1  32927  gsumvsca2  32928  isarchiofld  33026  prmidl2  33146  ssmxidl  33177  smatrcl  33387  reff  33430  ordtconnlem1  33515  qqhval2  33573  esumpcvgval  33687  imambfm  33872  ballotlemsf1o  34123  signstfvneq0  34194  pconnconn  34831  connpconn  34835  cvmliftmo  34884  cvmlift2lem10  34912  cvmlift2lem12  34914  cvmlift3lem7  34925  mrsubff1  35114  msubff1  35156  ifscgr  35630  cgrxfr  35641  btwnconn1lem13  35685  ellines  35738  unblimceq0lem  35971  unbdqndv2  35976  irrdiff  36795  matunitlindflem1  37078  poimirlem4  37086  poimirlem13  37095  poimirlem14  37096  heicant  37117  opnmbllem0  37118  mblfinlem3  37121  itg2addnclem  37133  itg2addnc  37136  ftc1cnnc  37154  sstotbnd  37237  cntotbnd  37258  ismtyima  37265  heibor1lem  37271  heiborlem10  37282  bfp  37286  rrncmslem  37294  islshpsm  38441  lsatcmp  38464  islshpat  38478  lfl0f  38530  iscvlat2N  38785  ishlat3N  38815  3dim1  38929  islvol5  39041  lvoli2  39043  lncvrelatN  39243  lncmp  39245  paddasslem10  39291  pclfinclN  39412  pexmidlem8N  39439  idltrn  39612  cdleme42keg  39948  cdleme42mgN  39950  cdlemf2  40024  cdlemg2cex  40053  trlcoat  40185  tendoex  40437  erngdvlem4  40453  erngdvlem4-rN  40461  dialss  40508  dibglbN  40628  diblss  40632  dihlsscpre  40696  dihglblem2aN  40755  dihglblem4  40759  dihglblem5  40760  dih1dimatlem  40791  dihglblem6  40802  lcfl7N  40963  lcfrlem9  41012  mapdh9a  41251  hdmapglem7  41391  aks4d1p8  41547  isprimroot  41553  evl1gprodd  41573  hashnexinjle  41584  deg1gprod  41596  sticksstones22  41624  imacrhmcl  41723  fsuppind  41795  renegeulemv  41895  sn-subeu  41953  remulinvcom  41959  sn-itrere  41993  sn-retire  41994  prjspertr  42001  prjspreln0  42005  flt4lem7  42055  nna4b4nsq  42056  isnacs3  42102  nacsfix  42104  mzpsubst  42140  eldioph2lem2  42153  eldioph2  42154  eldioph2b  42155  diophin  42164  diophun  42165  rencldnfilem  42212  irrapxlem3  42216  irrapxlem5  42218  pell1234qrreccl  42246  pell1234qrmulcl  42247  pell1qrge1  42262  pell1qrgaplem  42265  monotuz  42334  monotoddzzfi  42335  acongtr  42371  acongrep  42373  jm2.26a  42393  jm2.26lem3  42394  jm2.26  42395  jm2.27b  42399  jm2.27  42401  wepwsolem  42438  fnwe2lem2  42447  hbtlem5  42524  hbt  42526  mpaaeu  42546  cantnftermord  42721  cantnfresb  42725  omabs2  42733  tfsconcatun  42738  tfsconcatfn  42739  tfsconcatfv1  42740  tfsconcatfv2  42741  tfsconcatfv  42742  tfsconcatrn  42743  naddcnff  42763  oaun3lem1  42775  rfovcnvf1od  43406  mnurndlem1  43690  fnchoice  44363  rfcnnnub  44370  disjxp1  44405  ioondisj2  44850  iccintsng  44880  fprodcn  44960  lptioo2  44991  lptioo1  44992  limclner  45011  dvdsn1add  45299  stoweidlem14  45374  stoweidlem27  45387  stoweidlem34  45394  stoweidlem49  45409  stoweidlem56  45416  fourierdlem87  45553  iundjiun  45820  ismeannd  45827  hoidmvle  45960  prproropf1olem2  46816  perfectALTVlem2  47034  mogoldbb  47097  bgoldbtbndlem2  47118  bgoldbtbndlem3  47119  rngcinvALTV  47310  ringcinvALTV  47344  mndpsuppss  47407  lindslinindsimp2lem5  47502  itscnhlinecirc02p  47830  toslat  47965  functhinclem4  48022