Theorem simprrl 780

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 482	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 729	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4869  f1prex  7259  fpr3g  8264  fprresex  8289  nnaordex2  8603  naddssim  8649  eroveu  8785  mapdom2  9112  domunfican  9272  fofinf1o  9283  finsschain  9310  wemaplem3  9501  oemapvali  9637  iunfictbso  10067  enfin2i  10274  fin1a2s  10367  ttukeylem6  10467  distrlem4pr  10979  mulcmpblnr  11024  prsrlem1  11025  dedekind  11337  divdivdiv  11883  divmuleq  11887  divsubdiv  11898  lediv12a  12076  xralrple  13165  ssfzo12bi  13722  seqcaopr  14004  leexp2r  14139  hashbclem  14417  wrd2ind  14688  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  rtrclind  15031  rlimresb  15531  summo  15683  fsum2dlem  15736  prodmo  15902  fprod2dlem  15946  bezoutlem3  16511  bezoutlem4  16512  ncoprmgcdne1b  16620  qredeu  16628  coprmproddvdslem  16632  prmdvdsncoprmbd  16697  pcqmul  16824  pcadd  16860  pockthg  16877  prmreclem2  16888  vdwlem10  16961  ramub1lem2  16998  prmgaplem6  17027  prmgaplem7  17028  cshwsdisj  17069  mreexexlem4d  17608  mreexdomd  17610  issubc3  17811  cofucl  17850  setcmon  18049  setcepi  18050  drsdirfi  18266  poslubmo  18370  posglbmo  18371  grprida  18602  rabsubmgmd  18631  issubmd  18733  mndind  18755  ghmpreima  19170  gaorber  19240  psgnunilem4  19427  psgneu  19436  odcau  19534  pgpssslw  19544  fislw  19555  lsmsubm  19583  efgsfo  19669  gsum2d2  19904  pgpfac1lem5  20011  pgpfac1  20012  pgpfaclem2  20014  pgpfaclem3  20015  unitgrp  20292  lmodprop2d  20830  lsspropd  20924  lbsextlem4  21071  assapropd  21781  evlslem1  21989  mdetunilem8  22506  mdetuni0  22508  mdetmul  22510  neiint  22991  restbas  23045  iscnp4  23150  cnpco  23154  nrmsep  23244  regsep2  23263  ordthauslem  23270  1stcfb  23332  1stcrest  23340  2ndcctbss  23342  2ndcdisj  23343  2ndcomap  23345  dis2ndc  23347  nlly2i  23363  islly2  23371  hausllycmp  23381  lly1stc  23383  comppfsc  23419  ptbasin  23464  txcls  23491  ptcnp  23509  txlly  23523  txnlly  23524  txtube  23527  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  basqtop  23598  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  reghmph  23680  nrmhmph  23681  opnfbas  23729  rnelfmlem  23839  fmufil  23846  fclscf  23912  fclsfnflim  23914  flimfnfcls  23915  uffclsflim  23918  cnpfcfi  23927  cnpfcf  23928  alexsubALTlem2  23935  alexsubALTlem4  23937  tgpconncompeqg  23999  ghmcnp  24002  qustgplem  24008  tsmsxp  24042  blssps  24312  blss  24313  blcld  24393  metequiv2  24398  met2ndci  24410  prdsxmslem2  24417  txmetcnp  24435  nlmvscnlem1  24574  xrge0tsms  24723  ipcnlem1  25145  iscmet3  25193  metsscmetcld  25215  minveclem3  25329  pmltpc  25351  ovolscalem2  25415  ovolicc2lem5  25422  ovolicc2  25423  nulmbl2  25437  ioombl1  25463  uniioombllem6  25489  uniioombl  25490  vitalilem3  25511  i1faddlem  25594  mbfmullem  25626  itg2split  25650  lhop2  25920  dvfsumrlim  25938  itgsubst  25956  plydivex  26205  plyexmo  26221  ulmbdd  26307  cxploglim  26888  dchrptlem2  27176  lgsquad2lem2  27296  2sqlem5  27333  dchrvmasumif  27414  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  dchrmusum  27435  dchrvmasum  27436  pntibndlem3  27503  pntlemp  27521  ostth3  27549  nosupbday  27617  nosupbnd1lem1  27620  nosupbnd2  27628  noinfno  27630  noinfbday  27632  noinfbnd1lem1  27635  noinfbnd2  27643  conway  27711  madebdaylemlrcut  27810  mulsproplem9  28027  mulsproplem13  28031  mulsproplem14  28032  mulsuniflem  28052  uzsind  28293  readdscl  28350  legtrid  28518  hlcgreu  28545  mirreu3  28581  midexlem  28619  opphllem  28662  mideulem  28663  opphllem1  28674  oppperpex  28680  lnperpex  28730  trgcopy  28731  iscgra1  28737  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  acopyeu  28761  ax5seglem9  28864  ax5seg  28865  axcontlem8  28898  axcontlem12  28902  clwwlknonwwlknonb  30035  2pthfrgr  30213  frgrnbnb  30222  ablo4  30479  smcnlem  30626  pjhthmo  31231  mdslmd1lem1  32254  xrge0tsmsd  33002  locfinref  33831  xpinpreima2  33897  qqhval2  33972  dya2iocnrect  34272  orvcgteel  34459  orvclteel  34464  derangenlem  35158  cnpconn  35217  txpconn  35219  connpconn  35222  pconnpi1  35224  iccllysconn  35237  rellysconn  35238  cvmcov2  35262  cvmliftmolem2  35269  cvmliftmo  35271  cvmliftlem15  35285  cvmliftpht  35305  cvmlift3lem2  35307  cgrextend  35996  btwnouttr2  36010  cgrsub  36033  cgrxfr  36043  btwnxfr  36044  colineardim1  36049  btwnconn1lem6  36080  btwnconn1lem13  36087  btwnconn1lem14  36088  btwnconn3  36091  seglecgr12im  36098  segleantisym  36103  outsideofeq  36118  outsidele  36120  lineunray  36135  linethru  36141  fnessref  36345  neibastop2lem  36348  neibastop2  36349  weiunpo  36453  unblimceq0lem  36494  knoppndvlem22  36521  bj-finsumval0  37273  isbasisrelowllem1  37343  isbasisrelowllem2  37344  mblfinlem3  37653  cnambfre  37662  areacirclem5  37706  istotbnd3  37765  sstotbnd  37769  crngm4  37997  cvlcvr1  39332  4atlem12  39606  paddasslem10  39823  paddasslem12  39825  paddasslem13  39826  lhpexle3lem  40005  cdlemd4  40195  cdleme0cq  40209  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme32d  40438  cdleme32f  40440  cdleme40m  40461  cdleme40n  40462  cdleme42keg  40480  cdleme42mgN  40482  cdleme50trn2  40545  cdleme50trn3  40547  cdlemm10N  41112  dihvalcqpre  41229  dihopelvalcpre  41242  dihmeetlem1N  41284  dihjat1lem  41422  mapd0  41659  mapdh9a  41783  fsuppssind  42581  nna4b4nsq  42648  diophin  42760  pellexlem3  42819  pellexlem5  42821  pellex  42823  pell14qrmulcl  42851  jm2.19lem3  42980  jm2.25  42988  jm2.27b  42995  lmhmfgsplit  43075  hbtlem2  43113  hbtlem5  43117  gsumws3  44185  gsumws4  44186  mnuprdlem4  44264  fnchoice  45023  stoweidlem17  46015  stoweidlem53  46051  stoweidlem61  46059  qndenserrnbllem  46292  bgoldbtbnd  47810  cycldlenngric  47928  isubgr3stgrlem6  47970  lindslinindsimp1  48446  brab2dd  48816  prsthinc  49453