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  4875  f1prex  7293  fpr3g  8291  fprresex  8316  nnaordex2  8634  naddssim  8681  eroveu  8819  mapdom2  9146  domunfican  9291  fofinf1o  9299  finsschain  9326  wemaplem3  9520  oemapvali  9663  iunfictbso  10117  enfin2i  10323  fin1a2s  10416  ttukeylem6  10516  distrlem4pr  11029  mulcmpblnr  11074  prsrlem1  11075  dedekind  11391  divdivdiv  11934  divmuleq  11938  divsubdiv  11949  lediv12a  12126  xralrple  13249  ssfzo12bi  13809  seqcaopr  14095  leexp2r  14230  hashbclem  14509  wrd2ind  14784  rtrclreclem3  15123  rtrclreclem4  15124  relexpindlem  15126  rtrclind  15128  rlimresb  15642  summo  15794  fsum2dlem  15847  prodmo  16016  fprod2dlem  16060  bezoutlem3  16624  bezoutlem4  16625  ncoprmgcdne1b  16733  qredeu  16741  coprmproddvdslem  16745  prmdvdsncoprmbd  16811  pcqmul  16938  pcadd  16974  pockthg  16991  prmreclem2  17002  vdwlem10  17075  ramub1lem2  17112  prmgaplem6  17141  prmgaplem7  17142  cshwsdisj  17183  mreexexlem4d  17728  mreexdomd  17730  issubc3  17931  cofucl  17970  setcmon  18169  setcepi  18170  drsdirfi  18386  poslubmo  18490  posglbmo  18491  grprida  18759  rabsubmgmd  18791  issubmd  18895  mndind  18918  ghmpreima  19339  gaorber  19409  psgnunilem4  19598  psgneu  19607  odcau  19705  pgpssslw  19715  fislw  19726  lsmsubm  19754  efgsfo  19840  gsum2d2  20075  pgpfac1lem5  20182  pgpfac1  20183  pgpfaclem2  20185  pgpfaclem3  20186  unitgrp  20498  lmodprop2d  21082  lsspropd  21175  lbsextlem4  21322  assapropd  22058  evlslem1  22270  mdetunilem8  22813  mdetuni0  22815  mdetmul  22817  neiint  23298  restbas  23352  iscnp4  23457  cnpco  23461  nrmsep  23551  regsep2  23570  ordthauslem  23577  1stcfb  23639  1stcrest  23647  2ndcctbss  23649  2ndcdisj  23650  2ndcomap  23652  dis2ndc  23654  nlly2i  23670  islly2  23678  hausllycmp  23688  lly1stc  23690  comppfsc  23726  ptbasin  23771  txcls  23798  ptcnp  23816  txlly  23830  txnlly  23831  txtube  23834  txcmplem1  23835  txcmplem2  23836  xkococnlem  23853  basqtop  23905  regr1lem  23933  kqreglem1  23935  kqreglem2  23936  kqnrmlem1  23937  kqnrmlem2  23938  reghmph  23987  nrmhmph  23988  opnfbas  24036  rnelfmlem  24146  fmufil  24153  fclscf  24219  fclsfnflim  24221  flimfnfcls  24222  uffclsflim  24225  cnpfcfi  24234  cnpfcf  24235  alexsubALTlem2  24242  alexsubALTlem4  24244  tgpconncompeqg  24306  ghmcnp  24309  qustgplem  24315  tsmsxp  24349  blssps  24618  blss  24619  blcld  24699  metequiv2  24704  met2ndci  24716  prdsxmslem2  24723  txmetcnp  24741  nlmvscnlem1  24880  xrge0tsms  25029  ipcnlem1  25441  iscmet3  25489  metsscmetcld  25511  minveclem3  25625  pmltpc  25646  ovolscalem2  25710  ovolicc2lem5  25717  ovolicc2  25718  nulmbl2  25732  ioombl1  25758  uniioombllem6  25784  uniioombl  25785  vitalilem3  25806  i1faddlem  25889  mbfmullem  25921  itg2split  25945  lhop2  26211  dvfsumrlim  26227  itgsubst  26245  plydivex  26495  plyexmo  26511  ulmbdd  26598  cxploglim  27179  dchrptlem2  27466  lgsquad2lem2  27586  2sqlem5  27623  dchrvmasumif  27704  rpvmasum2  27713  dchrisum0re  27714  dchrisum0lem3  27720  dchrisum0  27721  dchrmusum  27725  dchrvmasum  27726  pntibndlem3  27793  pntlemp  27811  ostth3  27839  nosupbday  27906  nosupbnd1lem1  27909  nosupbnd2  27917  noinfno  27919  noinfbday  27921  noinfbnd1lem1  27924  noinfbnd2  27932  conway  28009  madebdaylemlrcut  28129  mulsproplem9  28354  mulsproplem13  28358  mulsproplem14  28359  mulsuniflem  28379  uzsind  28635  bdayfinbndlem1  28697  readdscl  28729  legtrid  28897  hlcgreu  28927  mirreu3  28968  midexlem  29006  opphllem  29053  mideulem  29054  opphllem1  29065  oppperpex  29071  lnperpex  29150  trgcopy  29152  iscgra1  29158  cgraswap  29168  cgracom  29170  cgratr  29171  flatcgra  29172  acopyeu  29182  ax5seglem9  29324  ax5seg  29325  axcontlem8  29358  axcontlem12  29362  clwwlknonwwlknonb  30494  2pthfrgr  30672  frgrnbnb  30681  ablo4  30939  smcnlem  31086  pjhthmo  31691  mdslmd1lem1  32714  xrge0tsmsd  33424  locfinref  34262  xpinpreima2  34328  qqhval2  34403  dya2iocnrect  34703  orvcgteel  34890  orvclteel  34895  derangenlem  35684  cnpconn  35743  txpconn  35745  connpconn  35748  pconnpi1  35750  iccllysconn  35763  rellysconn  35764  cvmcov2  35788  cvmliftmolem2  35795  cvmliftmo  35797  cvmliftlem15  35811  cvmliftpht  35831  cvmlift3lem2  35833  cgrextend  36521  btwnouttr2  36535  cgrsub  36558  cgrxfr  36568  btwnxfr  36569  colineardim1  36574  btwnconn1lem6  36605  btwnconn1lem13  36612  btwnconn1lem14  36613  btwnconn3  36616  seglecgr12im  36623  segleantisym  36628  outsideofeq  36643  outsidele  36645  lineunray  36660  linethru  36666  fnessref  36909  neibastop2lem  36912  neibastop2  36913  weiunpo  37017  unblimceq0lem  37136  knoppndvlem22  37163  bj-finsumval0  37970  isbasisrelowllem1  38042  isbasisrelowllem2  38043  mblfinlem3  38351  cnambfre  38360  areacirclem5  38404  istotbnd3  38463  sstotbnd  38467  crngm4  38695  cvlcvr1  40154  4atlem12  40427  paddasslem10  40644  paddasslem12  40646  paddasslem13  40647  lhpexle3lem  40826  cdlemd4  41016  cdleme0cq  41030  cdlemefs32sn1aw  41229  cdleme43fsv1snlem  41235  cdleme32d  41259  cdleme32f  41261  cdleme40m  41282  cdleme40n  41283  cdleme42keg  41301  cdleme42mgN  41303  cdleme50trn2  41366  cdleme50trn3  41368  cdlemm10N  41933  dihvalcqpre  42050  dihopelvalcpre  42063  dihmeetlem1N  42105  dihjat1lem  42243  mapd0  42480  mapdh9a  42604  fsuppssind  43366  nna4b4nsq  43433  diophin  43544  pellexlem3  43599  pellexlem5  43601  pellex  43603  pell14qrmulcl  43631  jm2.19lem3  43759  jm2.25  43767  jm2.27b  43774  lmhmfgsplit  43854  hbtlem2  43892  hbtlem5  43896  gsumws3  44963  gsumws4  44964  mnuprdlem4  45026  fnchoice  45790  stoweidlem17  46772  stoweidlem53  46808  stoweidlem61  46816  qndenserrnbllem  47049  bgoldbtbnd  48615  cycldlenngric  48734  isubgr3stgrlem6  48777  lindslinindsimp1  49278  brab2dd  49647  prsthinc  50283