Theorem simplrl 789

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5111  frpomin  6348  f1imass  7269  f1prex  7293  soisoi  7337  riota5f  7408  frxp3  8156  xpord3pred  8157  tfrlem9a  8382  oeeui  8597  oaabs2  8644  omabs  8646  naddssim  8681  omxpenlem  9076  fopwdom  9083  frfi  9255  marypha1lem  9403  ordiso2  9487  oismo  9512  wemaplem3  9520  cantnf  9672  ttrclss  9699  isinffi  9997  dfac12lem2  10147  dfac12lem3  10148  infxp  10216  infmap2  10219  infpssrlem5  10309  fin23lem11  10319  fin23lem24  10324  fin23lem26  10327  isf32lem2  10356  isf32lem4  10358  fin1a2lem13  10414  fin1a2s  10416  ttukeylem5  10515  fpwwe2lem11  10644  fpwwe2lem12  10645  wunex2  10741  tskord  10783  prlem934  11036  mulcmpblnr  11074  dedekind  11391  addrid  11408  cnegex  11409  negeu  11465  add20  11744  divdivdiv  11934  ltmul12a  12089  lediv12a  12126  cru  12228  uzwo3  12985  xleadd1a  13297  xlemul1a  13332  ixxun  13406  ixxss12  13410  elfz0ubfz0  13679  mulexpz  14158  rpexpmord  14224  leexp1a  14231  expmulnbnd  14291  swrdccatin1  14786  pfxccatin12lem3  14793  pfxccat3  14795  abs3lem  15416  rexanre  15424  cau3lem  15432  lo1bdd2  15601  o1lo1  15614  rlimclim1  15622  rlimclim  15623  lo1resb  15641  o1resb  15643  rlimcn3  15667  o1of2  15690  o1rlimmul  15696  lo1add  15704  lo1mul  15705  isercolllem1  15742  climcau  15748  summolem2  15793  summo  15794  o1fsum  15891  prodmolem2  16015  qredeu  16741  isprm5  16791  pclem  16923  pcqmul  16938  pcexp  16944  pcneg  16959  pcprmpw2  16967  pcadd  16974  prmpwdvds  16989  4sqlem13  17042  vdwlem2  17067  vdwlem7  17072  vdwlem11  17076  vdwlem12  17077  ramval  17093  ramz2  17109  ramcl  17114  prmgaplem6  17141  cshwshashlem2  17181  imasval  17590  imasdsval  17594  mreexexd  17729  issubc3  17931  idfucl  17963  funcres2c  17985  fucpropd  18062  xpcval  18258  prfval  18280  evlfcl  18303  curf12  18308  curf1cl  18309  curf2  18310  curfcl  18313  curfuncf  18319  curf2ndf  18328  hof2val  18337  hofcl  18340  hofpropd  18348  yonedalem4a  18356  yonedainv  18362  poslubmo  18490  posglbmo  18491  isipodrs  18618  acsmapd  18635  acsinfd  18637  chnpof1  18711  mgmhmeql  18803  sgrppropd  18818  ismndd  18843  mndpropd  18846  mndpsuppss  18854  mhmeql  18916  mndind  18918  frmdup3lem  18956  mhmmnd  19161  issubg4  19243  ssnmz  19263  f1otrspeq  19548  psgneu  19607  sylow2blem3  19723  lsmdisj2  19783  pj1eu  19797  efgredlem  19848  frgpuplem  19873  frgpnabl  19976  dmdprdsplitlem  20140  pgpfac1lem3  20180  pgpfaclem3  20186  ablsimpgcygd  20209  rngpropd  20283  ringpropd  20404  dvdsrtr  20483  rngcinv  20773  ringcinv  20807  islmhm2  21196  lmhmpropd  21231  prmidl2  21503  prmirredlem  21659  psgndiflemA  21788  lsmcss  21879  dsmmlss  21931  uvcf1  21979  frlmup1  21985  assapropd  22058  evlslem1  22270  coe1tmmul2  22474  mamucl  22595  mamuass  22596  mamudi  22597  mamudir  22598  mamuvs1  22599  mamuvs2  22600  mamulid  22635  mamurid  22636  dmatsubcl  22692  dmatmulcl  22694  mdetunilem7  22812  mdetunilem9  22814  cramer0  22884  cpmatmcllem  22912  mat2pmatf1  22923  decpmatmul  22966  pmatcollpw1  22970  pm2mpf1lem  22988  pm2mpmhmlem2  23013  chpidmat  23041  cpmadugsumlemB  23068  cpmadugsumlemC  23069  toponmre  23287  restbas  23352  iscncl  23463  cnpdis  23487  lmcnp  23498  dishaus  23576  cmpcovf  23585  hauscmplem  23600  dfconn2  23613  clsconn  23624  2ndcctbss  23649  1stccnp  23656  islly2  23678  llyidm  23682  cldllycmp  23689  locfincmp  23720  kgentopon  23732  1stckgenlem  23747  ptpjpre1  23765  ptbasfi  23775  txcls  23798  ptpjopn  23806  xkoccn  23813  txcnp  23814  txcmpb  23838  xkoptsub  23848  xkoco2cn  23852  xkoinjcn  23881  qtopcn  23908  qtoprest  23911  regr1lem  23933  regr1lem2  23934  kqreglem1  23935  qtophmeo  24011  fgabs  24073  hauspwpwf1  24181  flimfnfcls  24222  fclscmp  24224  cnpfcf  24235  ptcmplem4  24249  ptcmplem5  24250  cnextfval  24256  cnextfun  24258  tmdgsum2  24290  tsmsval2  24324  utoptop  24428  utop3cls  24445  ismet2  24527  blin  24615  metss2lem  24705  methaus  24714  met1stc  24715  met2ndci  24716  metcnp  24735  metcnpi3  24740  metustto  24747  metustfbas  24751  nlmvscn  24881  nrginvrcn  24886  nghmcn  24939  xrsxmet  25004  reconnlem1  25021  reconn  25023  xrge0tsms  25029  xmetdcn2  25032  metdscn  25051  addcnlem  25059  mulc1cncf  25101  cncfco  25103  cnheiborlem  25150  cnheibor  25151  nmoleub2lem2  25312  ipcn  25442  iscfil3  25469  cfilfcls  25470  iscmet3  25489  caubl  25504  bcthlem5  25524  rrxdstprj1  25605  minveclem3b  25624  minveclem7  25631  pmltpc  25646  ovolshftlem1  25705  ovolscalem1  25709  ioombl1  25758  uniioombllem6  25784  dyadss  25790  dyaddisjlem  25791  dyadmax  25794  opnmbllem  25797  itg1addlem2  25893  itg2seq  25938  bddmulibl  26035  limcfval  26068  ellimc3  26075  limciun  26090  dveflem  26175  rolle  26186  dvlip2  26191  c1liplem1  26192  dvgt0lem1  26198  dvgt0  26200  dvlt0  26201  dvne0  26207  dvcnvre  26215  dvfsumrlimge0  26226  ftc1lem6  26237  itgsubst  26245  mdegmullem  26272  ply1domn  26318  fta1g  26364  fta1b  26366  dgrlem  26423  coeid  26432  plydivalg  26497  aannenlem1  26528  aalioulem6  26537  ulmcn  26599  mtestbdd  26605  abelthlem8  26639  efif1olem4  26747  chordthm  27039  xrlimcnp  27170  lgamgulmlem5  27234  isppw2  27316  fsumvma2  27415  perfectlem2  27431  lgsdilem  27525  lgsquad2lem2  27586  lgsquad3  27588  2sqlem5  27623  2sqlem9  27628  rpvmasumlem  27688  dchrisum0flb  27711  pntpbnd  27789  pntibndlem3  27793  pntlem3  27810  pntleml  27812  nosupbday  27906  noinfbday  27921  noetasuplem4  27937  noetainflem4  27941  noetalem1  27942  lesrec  28029  madebdaylemlrcut  28129  bdayons  28506  n0fincut  28585  eucliddivs  28606  bdayfinbndlem1  28697  remulscllem2  28731  tgjustc1  28781  tgjustc2  28782  tgbtwnconn1lem3  28880  legtrid  28897  tglinethru  28946  tglineintmo  28952  tglnpt2  28963  mirreu3  28968  perpcom  29030  footexALT  29035  footex  29038  mideu  29056  opphllem1  29065  lnopp2hpgb  29082  axsegcon  29314  axpasch  29328  axeuclidlem  29349  ecgrtg  29370  elntg  29371  eengtrkg  29373  upgr1eopALT  29504  usgredg4  29604  usgr1eop  29637  usgr1v  29643  subuhgr  29673  subumgr  29675  subusgr  29676  nbuhgr2vtx1edgb  29739  wwlksnext  30279  usgr2wspthon  30354  clwlkclwwlkf1  30398  clwwisshclwwslem  30402  n4cyclfrgr  30679  dlwwlknondlwlknonf1o  30753  vacn  31083  ubthlem1  31259  ubthlem3  31261  minvecolem7  31272  chocunii  31690  pjhthmo  31691  pjhthlem2  31781  nmopub2tALT  32298  nmfnleub2  32315  kbass5  32509  mdslmd1lem1  32714  mdslmd1lem2  32715  mdsymlem5  32796  fcobij  33102  xrofsup  33149  mgcf1o  33354  xrge0tsmsd  33424  symgcntz  33436  archiabllem2a  33545  isarchiofld  33550  gsumvsca1  33577  gsumvsca2  33578  ssmxidl  33788  mplvrpmrhm  33968  constrelextdg2  34168  smatrcl  34217  reff  34260  ordtconnlem1  34345  qqhval2  34403  esumpcvgval  34499  imambfm  34684  ballotlemsf1o  34936  signstfvneq0  34991  pconnconn  35744  connpconn  35748  cvmliftmo  35797  cvmlift2lem10  35825  cvmlift2lem12  35827  cvmlift3lem7  35838  mrsubff1  36027  msubff1  36069  ifscgr  36557  cgrxfr  36568  btwnconn1lem13  36612  ellines  36665  nmuladdss  36726  nadddilem4  36736  weiunso  37018  weiunfr  37019  unblimceq0lem  37136  unbdqndv2  37141  irrdiff  38011  qdiff  38012  matunitlindflem1  38308  poimirlem4  38316  poimirlem13  38325  poimirlem14  38326  heicant  38347  opnmbllem0  38348  mblfinlem3  38351  itg2addnclem  38363  itg2addnc  38366  ftc1cnnc  38384  sstotbnd  38467  cntotbnd  38488  ismtyima  38495  heibor1lem  38501  heiborlem10  38512  bfp  38516  rrncmslem  38524  islshpsm  39795  lsatcmp  39818  islshpat  39832  lfl0f  39884  iscvlat2N  40139  ishlat3N  40169  3dim1  40282  islvol5  40394  lvoli2  40396  lncvrelatN  40596  lncmp  40598  paddasslem10  40644  pclfinclN  40765  pexmidlem8N  40792  idltrn  40965  cdleme42keg  41301  cdleme42mgN  41303  cdlemf2  41377  cdlemg2cex  41406  trlcoat  41538  tendoex  41790  erngdvlem4  41806  erngdvlem4-rN  41814  dialss  41861  dibglbN  41981  diblss  41985  dihlsscpre  42049  dihglblem2aN  42108  dihglblem4  42112  dihglblem5  42113  dih1dimatlem  42144  dihglblem6  42155  lcfl7N  42316  lcfrlem9  42365  mapdh9a  42604  hdmapglem7  42744  aks4d1p8  42895  isprimroot  42901  evl1gprodd  42925  hashnexinjle  42937  deg1gprod  42948  sticksstones22  42976  grpods  43002  renegeulemv  43170  sn-subeu  43229  remulinvcom  43235  imacrhmcl  43329  fidomncyc  43344  fsuppind  43363  prjspertr  43378  prjspreln0  43382  flt4lem7  43432  nna4b4nsq  43433  isnacs3  43482  nacsfix  43484  mzpsubst  43520  eldioph2lem2  43533  eldioph2  43534  eldioph2b  43535  diophin  43544  diophun  43545  rencldnfilem  43588  irrapxlem3  43592  irrapxlem5  43594  pell1234qrreccl  43622  pell1234qrmulcl  43623  pell1qrge1  43638  pell1qrgaplem  43641  monotuz  43709  monotoddzzfi  43710  acongtr  43746  acongrep  43748  jm2.26a  43768  jm2.26lem3  43769  jm2.26  43770  jm2.27b  43774  jm2.27  43776  wepwsolem  43810  fnwe2lem2  43819  hbtlem5  43896  hbt  43898  mpaaeu  43918  cantnftermord  44088  cantnfresb  44092  omabs2  44100  tfsconcatun  44105  tfsconcatfn  44106  tfsconcatfv1  44107  tfsconcatfv2  44108  tfsconcatfv  44109  tfsconcatrn  44110  naddcnff  44130  oaun3lem1  44142  rfovcnvf1od  44771  mnurndlem1  45032  fnchoice  45790  rfcnnnub  45797  disjxp1  45830  ioondisj2  46250  iccintsng  46280  fprodcn  46357  lptioo2  46388  lptioo1  46389  limclner  46406  dvdsn1add  46694  stoweidlem14  46769  stoweidlem27  46782  stoweidlem34  46789  stoweidlem49  46804  stoweidlem56  46811  fourierdlem87  46948  iundjiun  47215  ismeannd  47222  hoidmvle  47355  prproropf1olem2  48294  nprmmul2  48318  perfectALTVlem2  48528  mogoldbb  48591  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  grimgrtri  48755  isubgr3stgrlem6  48777  rngcinvALTV  49082  ringcinvALTV  49116  lindslinindsimp2lem5  49283  itscnhlinecirc02p  49606  toslat  49801  iinfssclem3  49875  iinfssc  49876  iinfsubc  49877  discsubc  49883  iinfconstbas  49885  imasubc3  49975  upciclem4  49988  natoppf  50048  tposcurf1  50118  fucofvalg  50137  fuco22  50158  fuco22natlem  50164  functhinclem4  50266  functhincfun  50268  arweuthinc  50348  lanfval  50432  ranfval  50433  islmd  50484  iscmd  50485