Theorem simprrl 793

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrl	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 742	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:  prproe  4868  f1prex  7289  fpr3g  8288  fprresex  8313  nnaordex2  8631  naddssim  8678  eroveu  8816  mapdom2  9150  domunfican  9295  fofinf1o  9303  finsschain  9330  wemaplem3  9524  oemapvali  9667  iunfictbso  10121  enfin2i  10327  fin1a2s  10420  ttukeylem6  10520  distrlem4pr  11039  mulcmpblnr  11084  prsrlem1  11085  dedekind  11401  divdivdiv  11944  divmuleq  11948  divsubdiv  11959  lediv12a  12136  xralrple  13261  ssfzo12bi  13821  seqcaopr  14107  leexp2r  14242  hashbclem  14521  wrd2ind  14796  rtrclreclem3  15137  rtrclreclem4  15138  relexpindlem  15140  rtrclind  15142  rlimresb  15656  summo  15807  fsum2dlem  15860  prodmo  16029  fprod2dlem  16073  bezoutlem3  16637  bezoutlem4  16638  ncoprmgcdne1b  16746  qredeu  16754  coprmproddvdslem  16758  prmdvdsncoprmbd  16824  pcqmul  16951  pcadd  16987  pockthg  17004  prmreclem2  17015  vdwlem10  17088  ramub1lem2  17125  prmgaplem6  17154  prmgaplem7  17155  cshwsdisj  17196  mreexexlem4d  17741  mreexdomd  17743  issubc3  17944  cofucl  17983  setcmon  18182  setcepi  18183  drsdirfi  18399  poslubmo  18503  posglbmo  18504  mgmn0plusgf  18747  grprida  18775  rabsubmgmd  18812  issubmd  18920  mndind  18943  ghmpreima  19371  gaorber  19441  psgnunilem4  19630  psgneu  19639  odcau  19737  pgpssslw  19747  fislw  19758  lsmsubm  19786  efgsfo  19872  gsum2d2  20107  pgpfac1lem5  20214  pgpfac1  20215  pgpfaclem2  20217  pgpfaclem3  20218  unitgrp  20530  lmodprop2d  21114  lsspropd  21207  lbsextlem4  21354  assapropd  22092  evlslem1  22304  mdetunilem8  22847  mdetuni0  22849  mdetmul  22851  neiint  23335  restbas  23389  iscnp4  23494  cnpco  23498  nrmsep  23588  regsep2  23607  ordthauslem  23614  1stcfb  23676  1stcrest  23684  2ndcctbss  23687  2ndcdisj  23688  2ndcomap  23690  dis2ndc  23692  nlly2i  23708  islly2  23716  hausllycmp  23726  lly1stc  23728  comppfsc  23764  ptbasin  23809  txcls  23836  ptcnp  23854  txlly  23868  txnlly  23869  txtube  23872  txcmplem1  23873  txcmplem2  23874  xkococnlem  23891  basqtop  23943  regr1lem  23971  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  reghmph  24025  nrmhmph  24026  opnfbas  24074  rnelfmlem  24184  fmufil  24191  fclscf  24257  fclsfnflim  24259  flimfnfcls  24260  uffclsflim  24263  cnpfcfi  24272  cnpfcf  24273  alexsubALTlem2  24280  alexsubALTlem4  24282  tgpconncompeqg  24344  ghmcnp  24347  qustgplem  24353  tsmsxp  24387  blssps  24656  blss  24657  blcld  24737  metequiv2  24742  met2ndci  24754  prdsxmslem2  24761  txmetcnp  24779  nlmvscnlem1  24918  xrge0tsms  25067  ipcnlem1  25479  iscmet3  25527  metsscmetcld  25549  minveclem3  25663  pmltpc  25684  ovolscalem2  25748  ovolicc2lem5  25755  ovolicc2  25756  nulmbl2  25770  ioombl1  25796  uniioombllem6  25822  uniioombl  25823  vitalilem3  25844  i1faddlem  25927  mbfmullem  25959  itg2split  25983  lhop2  26249  dvfsumrlim  26265  itgsubst  26283  plydivex  26534  plyexmo  26552  ulmbdd  26641  cxploglim  27222  dchrptlem2  27509  lgsquad2lem2  27629  2sqlem5  27666  dchrvmasumif  27747  rpvmasum2  27756  dchrisum0re  27757  dchrisum0lem3  27763  dchrisum0  27764  dchrmusum  27768  dchrvmasum  27769  pntibndlem3  27836  pntlemp  27854  ostth3  27882  nosupbday  27949  nosupbnd1lem1  27952  nosupbnd2  27960  noinfno  27962  noinfbday  27964  noinfbnd1lem1  27967  noinfbnd2  27975  conway  28052  madebdaylemlrcut  28172  mulsproplem9  28397  mulsproplem13  28401  mulsproplem14  28402  mulsuniflem  28422  uzsind  28678  bdayfinbndlem1  28740  readdscl  28772  legtrid  28941  hlcgreu  28971  mirreu3  29013  midexlem  29051  opphllem  29098  mideulem  29099  opphllem1  29110  oppperpex  29116  lnperpex  29196  trgcopy  29198  iscgra1  29204  cgraswap  29214  cgracom  29216  cgratr  29217  flatcgra  29219  acopyeu  29229  cgrabasimass  29265  ax5seglem9  29402  ax5seg  29403  axcontlem8  29436  axcontlem12  29440  clwwlknonwwlknonb  30584  2pthfrgr  30772  frgrnbnb  30781  ablo4  31039  smcnlem  31186  pjhthmo  31791  mdslmd1lem1  32814  xrge0tsmsd  33521  locfinref  34359  xpinpreima2  34425  qqhval2  34500  dya2iocnrect  34800  orvcgteel  34987  orvclteel  34992  derangenlem  35758  cnpconn  35817  txpconn  35819  connpconn  35822  pconnpi1  35824  iccllysconn  35837  rellysconn  35838  cvmcov2  35862  cvmliftmolem2  35869  cvmliftmo  35871  cvmliftlem15  35885  cvmliftpht  35905  cvmlift3lem2  35907  cgrextend  36596  btwnouttr2  36610  cgrsub  36633  cgrxfr  36643  btwnxfr  36644  colineardim1  36649  btwnconn1lem6  36680  btwnconn1lem13  36687  btwnconn1lem14  36688  btwnconn3  36691  seglecgr12im  36698  segleantisym  36703  outsideofeq  36718  outsidele  36720  lineunray  36735  linethru  36741  fnessref  36984  neibastop2lem  36987  neibastop2  36988  weiunpo  37092  unblimceq0lem  37211  knoppndvlem22  37238  bj-finsumval0  38045  isbasisrelowllem1  38117  isbasisrelowllem2  38118  mblfinlem3  38416  cnambfre  38425  areacirclem5  38469  istotbnd3  38529  sstotbnd  38533  crngm4  38761  cvlcvr1  40220  4atlem12  40493  paddasslem10  40710  paddasslem12  40712  paddasslem13  40713  lhpexle3lem  40892  cdlemd4  41082  cdleme0cq  41096  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme32d  41325  cdleme32f  41327  cdleme40m  41348  cdleme40n  41349  cdleme42keg  41367  cdleme42mgN  41369  cdleme50trn2  41432  cdleme50trn3  41434  cdlemm10N  41999  dihvalcqpre  42116  dihopelvalcpre  42129  dihmeetlem1N  42171  dihjat1lem  42309  mapd0  42546  mapdh9a  42670  fsuppssind  43447  nna4b4nsq  43514  diophin  43625  pellexlem3  43680  pellexlem5  43682  pellex  43684  pell14qrmulcl  43712  jm2.19lem3  43840  jm2.25  43848  jm2.27b  43855  lmhmfgsplit  43935  hbtlem2  43973  hbtlem5  43977  gsumws3  45044  gsumws4  45045  mnuprdlem4  45107  fnchoice  45871  stoweidlem17  46853  stoweidlem53  46889  stoweidlem61  46897  qndenserrnbllem  47130  bgoldbtbnd  48733  cycldlenngric  48852  isubgr3stgrlem6  48895  lindslinindsimp1  49395  brab2dd  49764  prsthinc  50398