Theorem simplrl 777

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 728	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  5082  frpomin  6304  f1imass  7219  f1prex  7239  soisoi  7283  riota5f  7352  frxp3  8101  xpord3pred  8102  tfrlem9a  8325  oeeui  8538  oaabs2  8585  omabs  8587  naddssim  8621  omxpenlem  9016  fopwdom  9023  frfi  9195  marypha1lem  9346  ordiso2  9430  oismo  9455  wemaplem3  9463  cantnf  9614  ttrclss  9641  isinffi  9916  dfac12lem2  10067  dfac12lem3  10068  infxp  10136  infmap2  10139  infpssrlem5  10229  fin23lem11  10239  fin23lem24  10244  fin23lem26  10247  isf32lem2  10276  isf32lem4  10278  fin1a2lem13  10334  fin1a2s  10336  ttukeylem5  10435  fpwwe2lem11  10564  fpwwe2lem12  10565  wunex2  10661  tskord  10703  prlem934  10956  mulcmpblnr  10994  dedekind  11309  addrid  11326  cnegex  11327  negeu  11383  add20  11662  divdivdiv  11856  ltmul12a  12011  lediv12a  12049  cru  12151  uzwo3  12893  xleadd1a  13205  xlemul1a  13240  ixxun  13314  ixxss12  13318  elfz0ubfz0  13586  mulexpz  14064  rpexpmord  14130  leexp1a  14137  expmulnbnd  14197  swrdccatin1  14687  pfxccatin12lem3  14694  pfxccat3  14696  abs3lem  15301  rexanre  15309  cau3lem  15317  lo1bdd2  15486  o1lo1  15499  rlimclim1  15507  rlimclim  15508  lo1resb  15526  o1resb  15528  rlimcn3  15552  o1of2  15575  o1rlimmul  15581  lo1add  15589  lo1mul  15590  isercolllem1  15627  climcau  15633  summolem2  15678  summo  15679  o1fsum  15776  prodmolem2  15900  qredeu  16627  isprm5  16677  pclem  16809  pcqmul  16824  pcexp  16830  pcneg  16845  pcprmpw2  16853  pcadd  16860  prmpwdvds  16875  4sqlem13  16928  vdwlem2  16953  vdwlem7  16958  vdwlem11  16962  vdwlem12  16963  ramval  16979  ramz2  16995  ramcl  17000  prmgaplem6  17027  cshwshashlem2  17067  imasval  17475  imasdsval  17479  mreexexd  17614  issubc3  17816  idfucl  17848  funcres2c  17870  fucpropd  17947  xpcval  18143  prfval  18165  evlfcl  18188  curf12  18193  curf1cl  18194  curf2  18195  curfcl  18198  curfuncf  18204  curf2ndf  18213  hof2val  18222  hofcl  18225  hofpropd  18233  yonedalem4a  18241  yonedainv  18247  poslubmo  18375  posglbmo  18376  isipodrs  18503  acsmapd  18520  acsinfd  18522  chnpof1  18596  mgmhmeql  18684  sgrppropd  18699  ismndd  18724  mndpropd  18727  mndpsuppss  18733  mhmeql  18794  mndind  18796  frmdup3lem  18834  mhmmnd  19040  issubg4  19121  ssnmz  19141  f1otrspeq  19422  psgneu  19481  sylow2blem3  19597  lsmdisj2  19657  pj1eu  19671  efgredlem  19722  frgpuplem  19747  frgpnabl  19850  dmdprdsplitlem  20014  pgpfac1lem3  20054  pgpfaclem3  20060  ablsimpgcygd  20083  rngpropd  20155  ringpropd  20269  dvdsrtr  20348  rngcinv  20614  ringcinv  20648  islmhm2  21033  lmhmpropd  21068  prmirredlem  21452  psgndiflemA  21581  lsmcss  21672  dsmmlss  21724  uvcf1  21772  frlmup1  21778  assapropd  21851  evlslem1  22060  coe1tmmul2  22241  mamucl  22366  mamuass  22367  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  mamulid  22406  mamurid  22407  dmatsubcl  22463  dmatmulcl  22465  mdetunilem7  22583  mdetunilem9  22585  cramer0  22655  cpmatmcllem  22683  mat2pmatf1  22694  decpmatmul  22737  pmatcollpw1  22741  pm2mpf1lem  22759  pm2mpmhmlem2  22784  chpidmat  22812  cpmadugsumlemB  22839  cpmadugsumlemC  22840  toponmre  23058  restbas  23123  iscncl  23234  cnpdis  23258  lmcnp  23269  dishaus  23347  cmpcovf  23356  hauscmplem  23371  dfconn2  23384  clsconn  23395  2ndcctbss  23420  1stccnp  23427  islly2  23449  llyidm  23453  cldllycmp  23460  locfincmp  23491  kgentopon  23503  1stckgenlem  23518  ptpjpre1  23536  ptbasfi  23546  txcls  23569  ptpjopn  23577  xkoccn  23584  txcnp  23585  txcmpb  23609  xkoptsub  23619  xkoco2cn  23623  xkoinjcn  23652  qtopcn  23679  qtoprest  23682  regr1lem  23704  regr1lem2  23705  kqreglem1  23706  qtophmeo  23782  fgabs  23844  hauspwpwf1  23952  flimfnfcls  23993  fclscmp  23995  cnpfcf  24006  ptcmplem4  24020  ptcmplem5  24021  cnextfval  24027  cnextfun  24029  tmdgsum2  24061  tsmsval2  24095  utoptop  24199  utop3cls  24216  ismet2  24298  blin  24386  metss2lem  24476  methaus  24485  met1stc  24486  met2ndci  24487  metcnp  24506  metcnpi3  24511  metustto  24518  metustfbas  24522  nlmvscn  24652  nrginvrcn  24657  nghmcn  24710  xrsxmet  24775  reconnlem1  24792  reconn  24794  xrge0tsms  24800  xmetdcn2  24803  metdscn  24822  addcnlem  24830  mulc1cncf  24872  cncfco  24874  cnheiborlem  24921  cnheibor  24922  nmoleub2lem2  25083  ipcn  25213  iscfil3  25240  cfilfcls  25241  iscmet3  25260  caubl  25275  bcthlem5  25295  rrxdstprj1  25376  minveclem3b  25395  minveclem7  25402  pmltpc  25417  ovolshftlem1  25476  ovolscalem1  25480  ioombl1  25529  uniioombllem6  25555  dyadss  25561  dyaddisjlem  25562  dyadmax  25565  opnmbllem  25568  itg1addlem2  25664  itg2seq  25709  bddmulibl  25806  limcfval  25839  ellimc3  25846  limciun  25861  dveflem  25946  rolle  25957  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  dvgt0  25971  dvlt0  25972  dvne0  25978  dvcnvre  25986  dvfsumrlimge0  25997  ftc1lem6  26008  itgsubst  26016  mdegmullem  26043  ply1domn  26089  fta1g  26135  fta1b  26137  dgrlem  26194  coeid  26203  plydivalg  26265  aannenlem1  26294  aalioulem6  26303  ulmcn  26364  mtestbdd  26370  abelthlem8  26404  efif1olem4  26509  chordthm  26801  xrlimcnp  26932  lgamgulmlem5  26996  isppw2  27078  fsumvma2  27177  perfectlem2  27193  lgsdilem  27287  lgsquad2lem2  27348  lgsquad3  27350  2sqlem5  27385  2sqlem9  27390  rpvmasumlem  27450  dchrisum0flb  27473  pntpbnd  27551  pntibndlem3  27555  pntlem3  27572  pntleml  27574  nosupbday  27669  noinfbday  27684  noetasuplem4  27700  noetainflem4  27704  noetalem1  27705  lesrec  27791  madebdaylemlrcut  27891  bdayons  28268  n0fincut  28347  eucliddivs  28368  bdayfinbndlem1  28459  remulscllem2  28493  tgjustc1  28543  tgjustc2  28544  tgbtwnconn1lem3  28642  legtrid  28659  tglinethru  28704  tglnpt2  28709  tglineintmo  28710  mirreu3  28722  perpcom  28781  footexALT  28786  footex  28789  mideu  28806  opphllem1  28815  lnopp2hpgb  28831  axsegcon  28996  axpasch  29010  axeuclidlem  29031  ecgrtg  29052  elntg  29053  eengtrkg  29055  upgr1eopALT  29186  usgredg4  29286  usgr1eop  29319  usgr1v  29325  subuhgr  29355  subumgr  29357  subusgr  29358  nbuhgr2vtx1edgb  29421  wwlksnext  29961  usgr2wspthon  30036  clwlkclwwlkf1  30080  clwwisshclwwslem  30084  n4cyclfrgr  30361  dlwwlknondlwlknonf1o  30435  vacn  30765  ubthlem1  30941  ubthlem3  30943  minvecolem7  30954  chocunii  31372  pjhthmo  31373  pjhthlem2  31463  nmopub2tALT  31980  nmfnleub2  31997  kbass5  32191  mdslmd1lem1  32396  mdslmd1lem2  32397  mdsymlem5  32478  fcobij  32793  xrofsup  32840  mgcf1o  33063  xrge0tsmsd  33134  symgcntz  33146  archiabllem2a  33255  isarchiofld  33260  gsumvsca1  33287  gsumvsca2  33288  prmidl2  33501  ssmxidl  33534  mplvrpmrhm  33691  constrelextdg2  33891  smatrcl  33940  reff  33983  ordtconnlem1  34068  qqhval2  34126  esumpcvgval  34222  imambfm  34406  ballotlemsf1o  34658  signstfvneq0  34716  pconnconn  35413  connpconn  35417  cvmliftmo  35466  cvmlift2lem10  35494  cvmlift2lem12  35496  cvmlift3lem7  35507  mrsubff1  35696  msubff1  35738  ifscgr  36226  cgrxfr  36237  btwnconn1lem13  36281  ellines  36334  weiunso  36648  weiunfr  36649  unblimceq0lem  36766  unbdqndv2  36771  irrdiff  37640  qdiff  37641  matunitlindflem1  37937  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  heicant  37976  opnmbllem0  37977  mblfinlem3  37980  itg2addnclem  37992  itg2addnc  37995  ftc1cnnc  38013  sstotbnd  38096  cntotbnd  38117  ismtyima  38124  heibor1lem  38130  heiborlem10  38141  bfp  38145  rrncmslem  38153  islshpsm  39426  lsatcmp  39449  islshpat  39463  lfl0f  39515  iscvlat2N  39770  ishlat3N  39800  3dim1  39913  islvol5  40025  lvoli2  40027  lncvrelatN  40227  lncmp  40229  paddasslem10  40275  pclfinclN  40396  pexmidlem8N  40423  idltrn  40596  cdleme42keg  40932  cdleme42mgN  40934  cdlemf2  41008  cdlemg2cex  41037  trlcoat  41169  tendoex  41421  erngdvlem4  41437  erngdvlem4-rN  41445  dialss  41492  dibglbN  41612  diblss  41616  dihlsscpre  41680  dihglblem2aN  41739  dihglblem4  41743  dihglblem5  41744  dih1dimatlem  41775  dihglblem6  41786  lcfl7N  41947  lcfrlem9  41996  mapdh9a  42235  hdmapglem7  42375  aks4d1p8  42526  isprimroot  42532  evl1gprodd  42556  hashnexinjle  42568  deg1gprod  42579  sticksstones22  42607  grpods  42633  renegeulemv  42800  sn-subeu  42859  remulinvcom  42865  imacrhmcl  42959  fidomncyc  42980  fsuppind  43023  prjspertr  43038  prjspreln0  43042  flt4lem7  43092  nna4b4nsq  43093  isnacs3  43142  nacsfix  43144  mzpsubst  43180  eldioph2lem2  43193  eldioph2  43194  eldioph2b  43195  diophin  43204  diophun  43205  rencldnfilem  43248  irrapxlem3  43252  irrapxlem5  43254  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1qrge1  43298  pell1qrgaplem  43301  monotuz  43369  monotoddzzfi  43370  acongtr  43406  acongrep  43408  jm2.26a  43428  jm2.26lem3  43429  jm2.26  43430  jm2.27b  43434  jm2.27  43436  wepwsolem  43470  fnwe2lem2  43479  hbtlem5  43556  hbt  43558  mpaaeu  43578  cantnftermord  43748  cantnfresb  43752  omabs2  43760  tfsconcatun  43765  tfsconcatfn  43766  tfsconcatfv1  43767  tfsconcatfv2  43768  tfsconcatfv  43769  tfsconcatrn  43770  naddcnff  43790  oaun3lem1  43802  rfovcnvf1od  44431  mnurndlem1  44708  fnchoice  45460  rfcnnnub  45467  disjxp1  45500  ioondisj2  45923  iccintsng  45953  fprodcn  46030  lptioo2  46061  lptioo1  46062  limclner  46079  dvdsn1add  46367  stoweidlem14  46442  stoweidlem27  46455  stoweidlem34  46462  stoweidlem49  46477  stoweidlem56  46484  fourierdlem87  46621  iundjiun  46888  ismeannd  46895  hoidmvle  47028  prproropf1olem2  47964  nprmmul2  47988  perfectALTVlem2  48198  mogoldbb  48261  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  grimgrtri  48425  isubgr3stgrlem6  48447  rngcinvALTV  48752  ringcinvALTV  48786  lindslinindsimp2lem5  48938  itscnhlinecirc02p  49261  toslat  49457  iinfssclem3  49531  iinfssc  49532  iinfsubc  49533  discsubc  49539  iinfconstbas  49541  imasubc3  49631  upciclem4  49644  natoppf  49704  tposcurf1  49774  fucofvalg  49793  fuco22  49814  fuco22natlem  49820  functhinclem4  49922  functhincfun  49924  arweuthinc  50004  lanfval  50088  ranfval  50089  islmd  50140  iscmd  50141