Theorem simplrl 773

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 723	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  5067  frpomin  6228  f1imass  7118  f1prex  7136  soisoi  7179  riota5f  7241  tfrlem9a  8188  oeeui  8395  oaabs2  8439  omabs  8441  omxpenlem  8813  fopwdom  8820  frfi  8989  marypha1lem  9122  ordiso2  9204  oismo  9229  wemaplem3  9237  cantnf  9381  isinffi  9681  dfac12lem2  9831  dfac12lem3  9832  infxp  9902  infmap2  9905  infpssrlem5  9994  fin23lem11  10004  fin23lem24  10009  fin23lem26  10012  isf32lem2  10041  isf32lem4  10043  fin1a2lem13  10099  fin1a2s  10101  ttukeylem5  10200  fpwwe2lem11  10328  fpwwe2lem12  10329  wunex2  10425  tskord  10467  prlem934  10720  mulcmpblnr  10758  dedekind  11068  addid1  11085  cnegex  11086  negeu  11141  add20  11417  divdivdiv  11606  ltmul12a  11761  lediv12a  11798  cru  11895  uzwo3  12612  xleadd1a  12916  xlemul1a  12951  ixxun  13024  ixxss12  13028  elfz0ubfz0  13289  mulexpz  13751  rpexpmord  13814  leexp1a  13821  expmulnbnd  13878  swrdccatin1  14366  pfxccatin12lem3  14373  pfxccat3  14375  abs3lem  14978  rexanre  14986  cau3lem  14994  lo1bdd2  15161  o1lo1  15174  rlimclim1  15182  rlimclim  15183  lo1resb  15201  o1resb  15203  rlimcn3  15227  o1of2  15250  o1rlimmul  15256  lo1add  15264  lo1mul  15265  isercolllem1  15304  climcau  15310  summolem2  15356  summo  15357  o1fsum  15453  prodmolem2  15573  qredeu  16291  isprm5  16340  pclem  16467  pcqmul  16482  pcexp  16488  pcneg  16503  pcprmpw2  16511  pcadd  16518  prmpwdvds  16533  4sqlem13  16586  vdwlem2  16611  vdwlem7  16616  vdwlem11  16620  vdwlem12  16621  ramval  16637  ramz2  16653  ramcl  16658  prmgaplem6  16685  cshwshashlem2  16726  imasval  17139  imasdsval  17143  mreexexd  17274  issubc3  17480  idfucl  17512  funcres2c  17533  fucpropd  17611  xpcval  17810  prfval  17832  evlfcl  17856  curf12  17861  curf1cl  17862  curf2  17863  curfcl  17866  curfuncf  17872  curf2ndf  17881  hof2val  17890  hofcl  17893  hofpropd  17901  yonedalem4a  17909  yonedainv  17915  poslubmo  18044  posglbmo  18045  isipodrs  18170  acsmapd  18187  acsinfd  18189  ismndd  18322  mndpropd  18325  mhmeql  18379  mndind  18381  frmdup3lem  18420  mhmmnd  18612  issubg4  18689  ssnmz  18709  f1otrspeq  18970  psgneu  19029  sylow2blem3  19142  lsmdisj2  19203  pj1eu  19217  efgredlem  19268  frgpuplem  19293  frgpnabl  19391  dmdprdsplitlem  19555  pgpfac1lem3  19595  pgpfaclem3  19601  ablsimpgcygd  19624  ringpropd  19736  dvdsrtr  19809  islmhm2  20215  lmhmpropd  20250  prmirredlem  20606  psgndiflemA  20718  lsmcss  20809  dsmmlss  20861  uvcf1  20909  frlmup1  20915  assapropd  20986  evlslem1  21202  coe1tmmul2  21357  mamucl  21458  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  mamulid  21498  mamurid  21499  dmatsubcl  21555  dmatmulcl  21557  mdetunilem7  21675  mdetunilem9  21677  cramer0  21747  cpmatmcllem  21775  mat2pmatf1  21786  decpmatmul  21829  pmatcollpw1  21833  pm2mpf1lem  21851  pm2mpmhmlem2  21876  chpidmat  21904  cpmadugsumlemB  21931  cpmadugsumlemC  21932  toponmre  22152  restbas  22217  iscncl  22328  cnpdis  22352  lmcnp  22363  dishaus  22441  cmpcovf  22450  hauscmplem  22465  dfconn2  22478  clsconn  22489  2ndcctbss  22514  1stccnp  22521  islly2  22543  llyidm  22547  cldllycmp  22554  locfincmp  22585  kgentopon  22597  1stckgenlem  22612  ptpjpre1  22630  ptbasfi  22640  txcls  22663  ptpjopn  22671  xkoccn  22678  txcnp  22679  txcmpb  22703  xkoptsub  22713  xkoco2cn  22717  xkoinjcn  22746  qtopcn  22773  qtoprest  22776  regr1lem  22798  regr1lem2  22799  kqreglem1  22800  qtophmeo  22876  fgabs  22938  hauspwpwf1  23046  flimfnfcls  23087  fclscmp  23089  cnpfcf  23100  ptcmplem4  23114  ptcmplem5  23115  cnextfval  23121  cnextfun  23123  tmdgsum2  23155  tsmsval2  23189  utoptop  23294  utop3cls  23311  ismet2  23394  blin  23482  metss2lem  23573  methaus  23582  met1stc  23583  met2ndci  23584  metcnp  23603  metcnpi3  23608  metustto  23615  metustfbas  23619  nlmvscn  23757  nrginvrcn  23762  nghmcn  23815  xrsxmet  23878  reconnlem1  23895  reconn  23897  xrge0tsms  23903  xmetdcn2  23906  metdscn  23925  addcnlem  23933  mulc1cncf  23974  cncfco  23976  cnheiborlem  24023  cnheibor  24024  nmoleub2lem2  24185  ipcn  24315  iscfil3  24342  cfilfcls  24343  iscmet3  24362  caubl  24377  bcthlem5  24397  rrxdstprj1  24478  minveclem3b  24497  minveclem7  24504  pmltpc  24519  ovolshftlem1  24578  ovolscalem1  24582  ioombl1  24631  uniioombllem6  24657  dyadss  24663  dyaddisjlem  24664  dyadmax  24667  opnmbllem  24670  itg1addlem2  24766  itg2seq  24812  bddmulibl  24908  limcfval  24941  ellimc3  24948  limciun  24963  dveflem  25048  rolle  25059  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  dvgt0  25073  dvlt0  25074  dvne0  25080  dvcnvre  25088  dvfsumrlimge0  25099  ftc1lem6  25110  itgsubst  25118  mdegmullem  25148  ply1domn  25193  fta1g  25237  fta1b  25239  dgrlem  25295  coeid  25304  plydivalg  25364  aannenlem1  25393  aalioulem6  25402  ulmcn  25463  mtestbdd  25469  abelthlem8  25503  efif1olem4  25606  chordthm  25892  xrlimcnp  26023  lgamgulmlem5  26087  isppw2  26169  fsumvma2  26267  perfectlem2  26283  lgsdilem  26377  lgsquad2lem2  26438  lgsquad3  26440  2sqlem5  26475  2sqlem9  26480  rpvmasumlem  26540  dchrisum0flb  26563  pntpbnd  26641  pntibndlem3  26645  pntlem3  26662  pntleml  26664  tgjustc1  26740  tgjustc2  26741  tgbtwnconn1lem3  26839  legtrid  26856  tglinethru  26901  tglnpt2  26906  tglineintmo  26907  mirreu3  26919  perpcom  26978  footexALT  26983  footex  26986  mideu  27003  opphllem1  27012  lnopp2hpgb  27028  axsegcon  27198  axpasch  27212  axeuclidlem  27233  ecgrtg  27254  elntg  27255  eengtrkg  27257  upgr1eopALT  27390  usgredg4  27487  usgr1eop  27520  usgr1v  27526  subuhgr  27556  subumgr  27558  subusgr  27559  nbuhgr2vtx1edgb  27622  wwlksnext  28159  usgr2wspthon  28231  clwlkclwwlkf1  28275  clwwisshclwwslem  28279  n4cyclfrgr  28556  dlwwlknondlwlknonf1o  28630  vacn  28957  ubthlem1  29133  ubthlem3  29135  minvecolem7  29146  chocunii  29564  pjhthmo  29565  pjhthlem2  29655  nmopub2tALT  30172  nmfnleub2  30189  kbass5  30383  mdslmd1lem1  30588  mdslmd1lem2  30589  mdsymlem5  30670  fcobij  30959  xrofsup  30992  mgcf1o  31183  xrge0tsmsd  31219  symgcntz  31256  archiabllem2a  31350  gsumvsca1  31381  gsumvsca2  31382  isarchiofld  31418  prmidl2  31518  ssmxidl  31544  smatrcl  31648  reff  31691  ordtconnlem1  31776  qqhval2  31832  esumpcvgval  31946  imambfm  32129  ballotlemsf1o  32380  signstfvneq0  32451  pconnconn  33093  connpconn  33097  cvmliftmo  33146  cvmlift2lem10  33174  cvmlift2lem12  33176  cvmlift3lem7  33187  mrsubff1  33376  msubff1  33418  ttrclss  33706  frxp3  33724  naddssim  33764  nosupbday  33835  noinfbday  33850  noetasuplem4  33866  noetainflem4  33870  noetalem1  33871  slerec  33940  madebdaylemlrcut  34006  ifscgr  34273  cgrxfr  34284  btwnconn1lem13  34328  ellines  34381  unblimceq0lem  34613  unbdqndv2  34618  irrdiff  35424  matunitlindflem1  35700  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  heicant  35739  opnmbllem0  35740  mblfinlem3  35743  itg2addnclem  35755  itg2addnc  35758  ftc1cnnc  35776  sstotbnd  35860  cntotbnd  35881  ismtyima  35888  heibor1lem  35894  heiborlem10  35905  bfp  35909  rrncmslem  35917  islshpsm  36921  lsatcmp  36944  islshpat  36958  lfl0f  37010  iscvlat2N  37265  ishlat3N  37295  3dim1  37408  islvol5  37520  lvoli2  37522  lncvrelatN  37722  lncmp  37724  paddasslem10  37770  pclfinclN  37891  pexmidlem8N  37918  idltrn  38091  cdleme42keg  38427  cdleme42mgN  38429  cdlemf2  38503  cdlemg2cex  38532  trlcoat  38664  tendoex  38916  erngdvlem4  38932  erngdvlem4-rN  38940  dialss  38987  dibglbN  39107  diblss  39111  dihlsscpre  39175  dihglblem2aN  39234  dihglblem4  39238  dihglblem5  39239  dih1dimatlem  39270  dihglblem6  39281  lcfl7N  39442  lcfrlem9  39491  mapdh9a  39730  hdmapglem7  39870  aks4d1p8  40023  sticksstones22  40052  fsuppind  40202  renegeulemv  40272  sn-subeu  40329  remulinvcom  40335  itrere  40357  retire  40358  prjspertr  40365  prjspreln0  40369  flt4lem7  40412  nna4b4nsq  40413  isnacs3  40448  nacsfix  40450  mzpsubst  40486  eldioph2lem2  40499  eldioph2  40500  eldioph2b  40501  diophin  40510  diophun  40511  rencldnfilem  40558  irrapxlem3  40562  irrapxlem5  40564  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell1qrge1  40608  pell1qrgaplem  40611  monotuz  40679  monotoddzzfi  40680  acongtr  40716  acongrep  40718  jm2.26a  40738  jm2.26lem3  40739  jm2.26  40740  jm2.27b  40744  jm2.27  40746  wepwsolem  40783  fnwe2lem2  40792  hbtlem5  40869  hbt  40871  mpaaeu  40891  rfovcnvf1od  41501  mnurndlem1  41788  fnchoice  42461  rfcnnnub  42468  disjxp1  42506  ioondisj2  42921  iccintsng  42951  fprodcn  43031  lptioo2  43062  lptioo1  43063  limclner  43082  dvdsn1add  43370  stoweidlem14  43445  stoweidlem27  43458  stoweidlem34  43465  stoweidlem49  43480  stoweidlem56  43487  fourierdlem87  43624  iundjiun  43888  ismeannd  43895  hoidmvle  44028  prproropf1olem2  44844  perfectALTVlem2  45062  mogoldbb  45125  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  mgmhmeql  45245  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  mndpsuppss  45595  lindslinindsimp2lem5  45691  itscnhlinecirc02p  46019  toslat  46156  functhinclem4  46213