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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  disjxiun  5036  frpomin  6172  f1imass  7054  f1prex  7072  soisoi  7115  riota5f  7177  tfrlem9a  8100  oeeui  8308  oaabs2  8352  omabs  8354  omxpenlem  8724  fopwdom  8731  frfi  8894  marypha1lem  9027  ordiso2  9109  oismo  9134  wemaplem3  9142  cantnf  9286  isinffi  9573  dfac12lem2  9723  dfac12lem3  9724  infxp  9794  infmap2  9797  infpssrlem5  9886  fin23lem11  9896  fin23lem24  9901  fin23lem26  9904  isf32lem2  9933  isf32lem4  9935  fin1a2lem13  9991  fin1a2s  9993  ttukeylem5  10092  fpwwe2lem11  10220  fpwwe2lem12  10221  wunex2  10317  tskord  10359  prlem934  10612  mulcmpblnr  10650  dedekind  10960  addid1  10977  cnegex  10978  negeu  11033  add20  11309  divdivdiv  11498  ltmul12a  11653  lediv12a  11690  cru  11787  uzwo3  12504  xleadd1a  12808  xlemul1a  12843  ixxun  12916  ixxss12  12920  elfz0ubfz0  13181  mulexpz  13640  rpexpmord  13703  leexp1a  13710  expmulnbnd  13767  swrdccatin1  14255  pfxccatin12lem3  14262  pfxccat3  14264  abs3lem  14867  rexanre  14875  cau3lem  14883  lo1bdd2  15050  o1lo1  15063  rlimclim1  15071  rlimclim  15072  lo1resb  15090  o1resb  15092  rlimcn3  15116  o1of2  15139  o1rlimmul  15145  lo1add  15153  lo1mul  15154  isercolllem1  15193  climcau  15199  summolem2  15245  summo  15246  o1fsum  15340  prodmolem2  15460  qredeu  16178  isprm5  16227  pclem  16354  pcqmul  16369  pcexp  16375  pcneg  16390  pcprmpw2  16398  pcadd  16405  prmpwdvds  16420  4sqlem13  16473  vdwlem2  16498  vdwlem7  16503  vdwlem11  16507  vdwlem12  16508  ramval  16524  ramz2  16540  ramcl  16545  prmgaplem6  16572  cshwshashlem2  16613  imasval  16970  imasdsval  16974  mreexexd  17105  issubc3  17309  idfucl  17341  funcres2c  17362  fucpropd  17440  xpcval  17638  prfval  17660  evlfcl  17684  curf12  17689  curf1cl  17690  curf2  17691  curfcl  17694  curfuncf  17700  curf2ndf  17709  hof2val  17718  hofcl  17721  hofpropd  17729  yonedalem4a  17737  yonedainv  17743  poslubmo  17871  posglbmo  17872  isipodrs  17997  acsmapd  18014  acsinfd  18016  ismndd  18149  mndpropd  18152  mhmeql  18206  mndind  18208  frmdup3lem  18247  mhmmnd  18439  issubg4  18516  ssnmz  18536  f1otrspeq  18793  psgneu  18852  sylow2blem3  18965  lsmdisj2  19026  pj1eu  19040  efgredlem  19091  frgpuplem  19116  frgpnabl  19214  dmdprdsplitlem  19378  pgpfac1lem3  19418  pgpfaclem3  19424  ablsimpgcygd  19447  ringpropd  19554  dvdsrtr  19624  islmhm2  20029  lmhmpropd  20064  prmirredlem  20413  psgndiflemA  20517  lsmcss  20608  dsmmlss  20660  uvcf1  20708  frlmup1  20714  assapropd  20785  evlslem1  20996  coe1tmmul2  21151  mamucl  21252  mamuass  21253  mamudi  21254  mamudir  21255  mamuvs1  21256  mamuvs2  21257  mamulid  21292  mamurid  21293  dmatsubcl  21349  dmatmulcl  21351  mdetunilem7  21469  mdetunilem9  21471  cramer0  21541  cpmatmcllem  21569  mat2pmatf1  21580  decpmatmul  21623  pmatcollpw1  21627  pm2mpf1lem  21645  pm2mpmhmlem2  21670  chpidmat  21698  cpmadugsumlemB  21725  cpmadugsumlemC  21726  toponmre  21944  restbas  22009  iscncl  22120  cnpdis  22144  lmcnp  22155  dishaus  22233  cmpcovf  22242  hauscmplem  22257  dfconn2  22270  clsconn  22281  2ndcctbss  22306  1stccnp  22313  islly2  22335  llyidm  22339  cldllycmp  22346  locfincmp  22377  kgentopon  22389  1stckgenlem  22404  ptpjpre1  22422  ptbasfi  22432  txcls  22455  ptpjopn  22463  xkoccn  22470  txcnp  22471  txcmpb  22495  xkoptsub  22505  xkoco2cn  22509  xkoinjcn  22538  qtopcn  22565  qtoprest  22568  regr1lem  22590  regr1lem2  22591  kqreglem1  22592  qtophmeo  22668  fgabs  22730  hauspwpwf1  22838  flimfnfcls  22879  fclscmp  22881  cnpfcf  22892  ptcmplem4  22906  ptcmplem5  22907  cnextfval  22913  cnextfun  22915  tmdgsum2  22947  tsmsval2  22981  utoptop  23086  utop3cls  23103  ismet2  23185  blin  23273  metss2lem  23363  methaus  23372  met1stc  23373  met2ndci  23374  metcnp  23393  metcnpi3  23398  metustto  23405  metustfbas  23409  nlmvscn  23539  nrginvrcn  23544  nghmcn  23597  xrsxmet  23660  reconnlem1  23677  reconn  23679  xrge0tsms  23685  xmetdcn2  23688  metdscn  23707  addcnlem  23715  mulc1cncf  23756  cncfco  23758  cnheiborlem  23805  cnheibor  23806  nmoleub2lem2  23967  ipcn  24097  iscfil3  24124  cfilfcls  24125  iscmet3  24144  caubl  24159  bcthlem5  24179  rrxdstprj1  24260  minveclem3b  24279  minveclem7  24286  pmltpc  24301  ovolshftlem1  24360  ovolscalem1  24364  ioombl1  24413  uniioombllem6  24439  dyadss  24445  dyaddisjlem  24446  dyadmax  24449  opnmbllem  24452  itg1addlem2  24548  itg2seq  24594  bddmulibl  24690  limcfval  24723  ellimc3  24730  limciun  24745  dveflem  24830  rolle  24841  dvlip2  24846  c1liplem1  24847  dvgt0lem1  24853  dvgt0  24855  dvlt0  24856  dvne0  24862  dvcnvre  24870  dvfsumrlimge0  24881  ftc1lem6  24892  itgsubst  24900  mdegmullem  24930  ply1domn  24975  fta1g  25019  fta1b  25021  dgrlem  25077  coeid  25086  plydivalg  25146  aannenlem1  25175  aalioulem6  25184  ulmcn  25245  mtestbdd  25251  abelthlem8  25285  efif1olem4  25388  chordthm  25674  xrlimcnp  25805  lgamgulmlem5  25869  isppw2  25951  fsumvma2  26049  perfectlem2  26065  lgsdilem  26159  lgsquad2lem2  26220  lgsquad3  26222  2sqlem5  26257  2sqlem9  26262  rpvmasumlem  26322  dchrisum0flb  26345  pntpbnd  26423  pntibndlem3  26427  pntlem3  26444  pntleml  26446  tgjustc1  26520  tgjustc2  26521  tgbtwnconn1lem3  26619  legtrid  26636  tglinethru  26681  tglnpt2  26686  tglineintmo  26687  mirreu3  26699  perpcom  26758  footexALT  26763  footex  26766  mideu  26783  opphllem1  26792  lnopp2hpgb  26808  axsegcon  26972  axpasch  26986  axeuclidlem  27007  ecgrtg  27028  elntg  27029  eengtrkg  27031  upgr1eopALT  27162  usgredg4  27259  usgr1eop  27292  usgr1v  27298  subuhgr  27328  subumgr  27330  subusgr  27331  nbuhgr2vtx1edgb  27394  wwlksnext  27931  usgr2wspthon  28003  clwlkclwwlkf1  28047  clwwisshclwwslem  28051  n4cyclfrgr  28328  dlwwlknondlwlknonf1o  28402  vacn  28729  ubthlem1  28905  ubthlem3  28907  minvecolem7  28918  chocunii  29336  pjhthmo  29337  pjhthlem2  29427  nmopub2tALT  29944  nmfnleub2  29961  kbass5  30155  mdslmd1lem1  30360  mdslmd1lem2  30361  mdsymlem5  30442  fcobij  30731  xrofsup  30764  mgcf1o  30954  xrge0tsmsd  30990  symgcntz  31027  archiabllem2a  31121  gsumvsca1  31152  gsumvsca2  31153  isarchiofld  31189  prmidl2  31284  ssmxidl  31310  smatrcl  31414  reff  31457  ordtconnlem1  31542  qqhval2  31598  esumpcvgval  31712  imambfm  31895  ballotlemsf1o  32146  signstfvneq0  32217  pconnconn  32860  connpconn  32864  cvmliftmo  32913  cvmlift2lem10  32941  cvmlift2lem12  32943  cvmlift3lem7  32954  mrsubff1  33143  msubff1  33185  frxp3  33477  naddssim  33523  nosupbday  33594  noinfbday  33609  noetasuplem4  33625  noetainflem4  33629  noetalem1  33630  slerec  33699  madebdaylemlrcut  33765  ifscgr  34032  cgrxfr  34043  btwnconn1lem13  34087  ellines  34140  unblimceq0lem  34372  unbdqndv2  34377  irrdiff  35180  matunitlindflem1  35459  poimirlem4  35467  poimirlem13  35476  poimirlem14  35477  heicant  35498  opnmbllem0  35499  mblfinlem3  35502  itg2addnclem  35514  itg2addnc  35517  ftc1cnnc  35535  sstotbnd  35619  cntotbnd  35640  ismtyima  35647  heibor1lem  35653  heiborlem10  35664  bfp  35668  rrncmslem  35676  islshpsm  36680  lsatcmp  36703  islshpat  36717  lfl0f  36769  iscvlat2N  37024  ishlat3N  37054  3dim1  37167  islvol5  37279  lvoli2  37281  lncvrelatN  37481  lncmp  37483  paddasslem10  37529  pclfinclN  37650  pexmidlem8N  37677  idltrn  37850  cdleme42keg  38186  cdleme42mgN  38188  cdlemf2  38262  cdlemg2cex  38291  trlcoat  38423  tendoex  38675  erngdvlem4  38691  erngdvlem4-rN  38699  dialss  38746  dibglbN  38866  diblss  38870  dihlsscpre  38934  dihglblem2aN  38993  dihglblem4  38997  dihglblem5  38998  dih1dimatlem  39029  dihglblem6  39040  lcfl7N  39201  lcfrlem9  39250  mapdh9a  39489  hdmapglem7  39629  fsuppind  39930  renegeulemv  40000  sn-subeu  40057  remulinvcom  40063  itrere  40085  retire  40086  prjspertr  40093  prjspreln0  40097  flt4lem7  40140  nna4b4nsq  40141  isnacs3  40176  nacsfix  40178  mzpsubst  40214  eldioph2lem2  40227  eldioph2  40228  eldioph2b  40229  diophin  40238  diophun  40239  rencldnfilem  40286  irrapxlem3  40290  irrapxlem5  40292  pell1234qrreccl  40320  pell1234qrmulcl  40321  pell1qrge1  40336  pell1qrgaplem  40339  monotuz  40407  monotoddzzfi  40408  acongtr  40444  acongrep  40446  jm2.26a  40466  jm2.26lem3  40467  jm2.26  40468  jm2.27b  40472  jm2.27  40474  wepwsolem  40511  fnwe2lem2  40520  hbtlem5  40597  hbt  40599  mpaaeu  40619  rfovcnvf1od  41230  mnurndlem1  41513  fnchoice  42186  rfcnnnub  42193  disjxp1  42231  ioondisj2  42647  iccintsng  42677  fprodcn  42759  lptioo2  42790  lptioo1  42791  limclner  42810  dvdsn1add  43098  stoweidlem14  43173  stoweidlem27  43186  stoweidlem34  43193  stoweidlem49  43208  stoweidlem56  43215  fourierdlem87  43352  iundjiun  43616  ismeannd  43623  hoidmvle  43756  prproropf1olem2  44572  perfectALTVlem2  44790  mogoldbb  44853  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  mgmhmeql  44973  rngcinv  45155  rngcinvALTV  45167  ringcinv  45206  ringcinvALTV  45230  mndpsuppss  45323  lindslinindsimp2lem5  45419  itscnhlinecirc02p  45747  toslat  45884  functhinclem4  45941