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  4832  f1prex  7292  fpr3g  8306  fprresex  8331  nnaordex2  8651  naddssim  8698  eroveu  8836  mapdom2  9170  domunfican  9316  fofinf1o  9324  finsschain  9351  wemaplem3  9545  oemapvali  9688  iunfictbso  10196  enfin2i  10402  fin1a2s  10495  ttukeylem6  10595  distrlem4pr  11114  mulcmpblnr  11159  prsrlem1  11160  dedekind  11476  divdivdiv  12021  divmuleq  12025  divsubdiv  12036  lediv12a  12213  xralrple  13338  ssfzo12bi  13899  seqcaopr  14185  leexp2r  14320  hashbclem  14600  wrd2ind  14876  rtrclreclem3  15218  rtrclreclem4  15219  relexpindlem  15221  rtrclind  15223  rlimresb  15737  summo  15888  fsum2dlem  15941  prodmo  16108  fprod2dlem  16152  bezoutlem3  16719  bezoutlem4  16720  ncoprmgcdne1b  16830  qredeu  16838  coprmproddvdslem  16842  prmdvdsncoprmbd  16908  pcqmul  17036  pcadd  17072  pockthg  17089  prmreclem2  17100  vdwlem10  17173  ramub1lem2  17210  prmgaplem6  17239  prmgaplem7  17240  cshwsdisj  17281  mreexexlem4d  17826  mreexdomd  17828  issubc3  18029  cofucl  18068  setcmon  18267  setcepi  18268  drsdirfi  18484  poslubmo  18588  posglbmo  18589  mgmn0plusgf  18832  grprida  18861  rabsubmgmd  18898  issubmd  19006  mndind  19029  ghmpreima  19457  gaorber  19527  psgnunilem4  19716  psgneu  19725  odcau  19823  pgpssslw  19833  fislw  19844  lsmsubm  19872  efgsfo  19958  gsum2d2  20193  pgpfac1lem5  20300  pgpfac1  20301  pgpfaclem2  20303  pgpfaclem3  20304  unitgrp  20618  lmodprop2d  21204  lsspropd  21297  lbsextlem4  21444  assapropd  22184  evlslem1  22396  mdetunilem8  22939  mdetuni0  22941  mdetmul  22943  neiint  23427  restbas  23481  iscnp4  23586  cnpco  23590  nrmsep  23680  regsep2  23699  ordthauslem  23706  1stcfb  23768  1stcrest  23776  2ndcctbss  23779  2ndcdisj  23780  2ndcomap  23782  dis2ndc  23784  nlly2i  23800  islly2  23808  hausllycmp  23818  lly1stc  23820  comppfsc  23856  ptbasin  23901  txcls  23928  ptcnp  23946  txlly  23960  txnlly  23961  txtube  23964  txcmplem1  23965  txcmplem2  23966  xkococnlem  23983  basqtop  24035  regr1lem  24063  kqreglem1  24065  kqreglem2  24066  kqnrmlem1  24067  kqnrmlem2  24068  reghmph  24117  nrmhmph  24118  opnfbas  24166  rnelfmlem  24276  fmufil  24283  fclscf  24349  fclsfnflim  24351  flimfnfcls  24352  uffclsflim  24355  cnpfcfi  24364  cnpfcf  24365  alexsubALTlem2  24372  alexsubALTlem4  24374  tgpconncompeqg  24436  ghmcnp  24439  qustgplem  24445  tsmsxp  24479  blssps  24748  blss  24749  blcld  24829  metequiv2  24834  met2ndci  24846  prdsxmslem2  24853  txmetcnp  24871  nlmvscnlem1  25010  xrge0tsms  25159  ipcnlem1  25571  iscmet3  25619  metsscmetcld  25641  minveclem3  25755  pmltpc  25776  ovolscalem2  25840  ovolicc2lem5  25847  ovolicc2  25848  nulmbl2  25862  ioombl1  25888  uniioombllem6  25914  uniioombl  25915  vitalilem3  25936  i1faddlem  26019  mbfmullem  26051  itg2split  26075  lhop2  26340  dvfsumrlim  26356  itgsubst  26374  plydivex  26623  plyexmo  26641  ulmbdd  26730  cxploglim  27310  dchrptlem2  27597  lgsquad2lem2  27717  2sqlem5  27754  dchrvmasumif  27835  rpvmasum2  27844  dchrisum0re  27845  dchrisum0lem3  27851  dchrisum0  27852  dchrmusum  27856  dchrvmasum  27857  pntibndlem3  27924  pntlemp  27942  ostth3  27970  nna4b4nsq  27995  nosupbday  28067  nosupbnd1lem1  28070  nosupbnd2  28078  noinfno  28080  noinfbday  28082  noinfbnd1lem1  28085  noinfbnd2  28093  conway  28170  madebdaylemlrcut  28290  mulsproplem9  28515  mulsproplem13  28519  mulsproplem14  28520  mulsuniflem  28540  uzsind  28796  bdayfinbndlem1  28858  readdscl  28890  legtrid  29059  hlcgreu  29089  mirreu3  29131  midexlem  29169  opphllem  29216  mideulem  29217  opphllem1  29228  oppperpex  29234  lnperpex  29314  trgcopy  29316  iscgra1  29322  cgraswap  29332  cgracom  29334  cgratr  29335  flatcgra  29337  acopyeu  29347  cgrabasimass  29383  ax5seglem9  29520  ax5seg  29521  axcontlem8  29554  axcontlem12  29558  clwwlknonwwlknonb  30702  2pthfrgr  30890  frgrnbnb  30899  ablo4  31157  smcnlem  31304  pjhthmo  31909  mdslmd1lem1  32932  tgextahp  33078  xrge0tsmsd  33680  locfinref  34519  xpinpreima2  34585  qqhval2  34660  dya2iocnrect  34959  orvcgteel  35146  orvclteel  35151  derangenlem  36022  cnpconn  36081  txpconn  36083  connpconn  36086  pconnpi1  36088  iccllysconn  36101  rellysconn  36102  cvmcov2  36126  cvmliftmolem2  36133  cvmliftmo  36135  cvmliftlem15  36149  cvmliftpht  36169  cvmlift3lem2  36171  cgrextend  36865  btwnouttr2  36879  cgrsub  36902  cgrxfr  36912  btwnxfr  36913  colineardim1  36918  btwnconn1lem6  36949  btwnconn1lem13  36956  btwnconn1lem14  36957  btwnconn3  36960  seglecgr12im  36967  segleantisym  36972  outsideofeq  36987  outsidele  36989  lineunray  37004  linethru  37010  fnessref  37237  neibastop2lem  37240  neibastop2  37241  weiunpo  37345  unblimceq0lem  37464  knoppndvlem22  37491  bj-finsumval0  38299  isbasisrelowllem1  38371  isbasisrelowllem2  38372  mblfinlem3  38670  cnambfre  38679  areacirclem5  38723  istotbnd3  38798  sstotbnd  38802  crngm4  39030  cvlcvr1  40489  4atlem12  40762  paddasslem10  40979  paddasslem12  40981  paddasslem13  40982  lhpexle3lem  41161  cdlemd4  41351  cdleme0cq  41365  cdlemefs32sn1aw  41564  cdleme43fsv1snlem  41570  cdleme32d  41594  cdleme32f  41596  cdleme40m  41617  cdleme40n  41618  cdleme42keg  41636  cdleme42mgN  41638  cdleme50trn2  41701  cdleme50trn3  41703  cdlemm10N  42268  dihvalcqpre  42385  dihopelvalcpre  42398  dihmeetlem1N  42440  dihjat1lem  42578  mapd0  42815  mapdh9a  42939  fsuppssind  43714  diophin  43876  pellexlem3  43931  pellexlem5  43933  pellex  43935  pell14qrmulcl  43963  jm2.19lem3  44091  jm2.25  44099  jm2.27b  44106  lmhmfgsplit  44181  hbtlem2  44219  hbtlem5  44223  gsumws3  45289  gsumws4  45290  mnuprdlem4  45352  fnchoice  46139  stoweidlem17  47120  stoweidlem53  47156  stoweidlem61  47164  qndenserrnbllem  47397  bgoldbtbnd  49000  cycldlenngric  49119  isubgr3stgrlem6  49162  lindslinindsimp1  49662  brab2dd  50032  prsthinc  50692  parmapcl2  50863