Theorem simplrl 776

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  disjxiun  5146  frpomin  6342  f1imass  7263  f1prex  7282  soisoi  7325  riota5f  7394  frxp3  8137  xpord3pred  8138  tfrlem9a  8386  oeeui  8602  oaabs2  8648  omabs  8650  naddssim  8684  omxpenlem  9073  fopwdom  9080  frfi  9288  marypha1lem  9428  ordiso2  9510  oismo  9535  wemaplem3  9543  cantnf  9688  ttrclss  9715  isinffi  9987  dfac12lem2  10139  dfac12lem3  10140  infxp  10210  infmap2  10213  infpssrlem5  10302  fin23lem11  10312  fin23lem24  10317  fin23lem26  10320  isf32lem2  10349  isf32lem4  10351  fin1a2lem13  10407  fin1a2s  10409  ttukeylem5  10508  fpwwe2lem11  10636  fpwwe2lem12  10637  wunex2  10733  tskord  10775  prlem934  11028  mulcmpblnr  11066  dedekind  11377  addrid  11394  cnegex  11395  negeu  11450  add20  11726  divdivdiv  11915  ltmul12a  12070  lediv12a  12107  cru  12204  uzwo3  12927  xleadd1a  13232  xlemul1a  13267  ixxun  13340  ixxss12  13344  elfz0ubfz0  13605  mulexpz  14068  rpexpmord  14133  leexp1a  14140  expmulnbnd  14198  swrdccatin1  14675  pfxccatin12lem3  14682  pfxccat3  14684  abs3lem  15285  rexanre  15293  cau3lem  15301  lo1bdd2  15468  o1lo1  15481  rlimclim1  15489  rlimclim  15490  lo1resb  15508  o1resb  15510  rlimcn3  15534  o1of2  15557  o1rlimmul  15563  lo1add  15571  lo1mul  15572  isercolllem1  15611  climcau  15617  summolem2  15662  summo  15663  o1fsum  15759  prodmolem2  15879  qredeu  16595  isprm5  16644  pclem  16771  pcqmul  16786  pcexp  16792  pcneg  16807  pcprmpw2  16815  pcadd  16822  prmpwdvds  16837  4sqlem13  16890  vdwlem2  16915  vdwlem7  16920  vdwlem11  16924  vdwlem12  16925  ramval  16941  ramz2  16957  ramcl  16962  prmgaplem6  16989  cshwshashlem2  17030  imasval  17457  imasdsval  17461  mreexexd  17592  issubc3  17799  idfucl  17831  funcres2c  17852  fucpropd  17930  xpcval  18129  prfval  18151  evlfcl  18175  curf12  18180  curf1cl  18181  curf2  18182  curfcl  18185  curfuncf  18191  curf2ndf  18200  hof2val  18209  hofcl  18212  hofpropd  18220  yonedalem4a  18228  yonedainv  18234  poslubmo  18364  posglbmo  18365  isipodrs  18490  acsmapd  18507  acsinfd  18509  sgrppropd  18622  ismndd  18647  mndpropd  18650  mhmeql  18707  mndind  18709  frmdup3lem  18747  mhmmnd  18947  issubg4  19025  ssnmz  19046  f1otrspeq  19315  psgneu  19374  sylow2blem3  19490  lsmdisj2  19550  pj1eu  19564  efgredlem  19615  frgpuplem  19640  frgpnabl  19743  dmdprdsplitlem  19907  pgpfac1lem3  19947  pgpfaclem3  19953  ablsimpgcygd  19976  ringpropd  20102  dvdsrtr  20182  islmhm2  20649  lmhmpropd  20684  prmirredlem  21042  psgndiflemA  21154  lsmcss  21245  dsmmlss  21299  uvcf1  21347  frlmup1  21353  assapropd  21426  evlslem1  21645  coe1tmmul2  21798  mamucl  21901  mamuass  21902  mamudi  21903  mamudir  21904  mamuvs1  21905  mamuvs2  21906  mamulid  21943  mamurid  21944  dmatsubcl  22000  dmatmulcl  22002  mdetunilem7  22120  mdetunilem9  22122  cramer0  22192  cpmatmcllem  22220  mat2pmatf1  22231  decpmatmul  22274  pmatcollpw1  22278  pm2mpf1lem  22296  pm2mpmhmlem2  22321  chpidmat  22349  cpmadugsumlemB  22376  cpmadugsumlemC  22377  toponmre  22597  restbas  22662  iscncl  22773  cnpdis  22797  lmcnp  22808  dishaus  22886  cmpcovf  22895  hauscmplem  22910  dfconn2  22923  clsconn  22934  2ndcctbss  22959  1stccnp  22966  islly2  22988  llyidm  22992  cldllycmp  22999  locfincmp  23030  kgentopon  23042  1stckgenlem  23057  ptpjpre1  23075  ptbasfi  23085  txcls  23108  ptpjopn  23116  xkoccn  23123  txcnp  23124  txcmpb  23148  xkoptsub  23158  xkoco2cn  23162  xkoinjcn  23191  qtopcn  23218  qtoprest  23221  regr1lem  23243  regr1lem2  23244  kqreglem1  23245  qtophmeo  23321  fgabs  23383  hauspwpwf1  23491  flimfnfcls  23532  fclscmp  23534  cnpfcf  23545  ptcmplem4  23559  ptcmplem5  23560  cnextfval  23566  cnextfun  23568  tmdgsum2  23600  tsmsval2  23634  utoptop  23739  utop3cls  23756  ismet2  23839  blin  23927  metss2lem  24020  methaus  24029  met1stc  24030  met2ndci  24031  metcnp  24050  metcnpi3  24055  metustto  24062  metustfbas  24066  nlmvscn  24204  nrginvrcn  24209  nghmcn  24262  xrsxmet  24325  reconnlem1  24342  reconn  24344  xrge0tsms  24350  xmetdcn2  24353  metdscn  24372  addcnlem  24380  mulc1cncf  24421  cncfco  24423  cnheiborlem  24470  cnheibor  24471  nmoleub2lem2  24632  ipcn  24763  iscfil3  24790  cfilfcls  24791  iscmet3  24810  caubl  24825  bcthlem5  24845  rrxdstprj1  24926  minveclem3b  24945  minveclem7  24952  pmltpc  24967  ovolshftlem1  25026  ovolscalem1  25030  ioombl1  25079  uniioombllem6  25105  dyadss  25111  dyaddisjlem  25112  dyadmax  25115  opnmbllem  25118  itg1addlem2  25214  itg2seq  25260  bddmulibl  25356  limcfval  25389  ellimc3  25396  limciun  25411  dveflem  25496  rolle  25507  dvlip2  25512  c1liplem1  25513  dvgt0lem1  25519  dvgt0  25521  dvlt0  25522  dvne0  25528  dvcnvre  25536  dvfsumrlimge0  25547  ftc1lem6  25558  itgsubst  25566  mdegmullem  25596  ply1domn  25641  fta1g  25685  fta1b  25687  dgrlem  25743  coeid  25752  plydivalg  25812  aannenlem1  25841  aalioulem6  25850  ulmcn  25911  mtestbdd  25917  abelthlem8  25951  efif1olem4  26054  chordthm  26342  xrlimcnp  26473  lgamgulmlem5  26537  isppw2  26619  fsumvma2  26717  perfectlem2  26733  lgsdilem  26827  lgsquad2lem2  26888  lgsquad3  26890  2sqlem5  26925  2sqlem9  26930  rpvmasumlem  26990  dchrisum0flb  27013  pntpbnd  27091  pntibndlem3  27095  pntlem3  27112  pntleml  27114  nosupbday  27208  noinfbday  27223  noetasuplem4  27239  noetainflem4  27243  noetalem1  27244  slerec  27320  madebdaylemlrcut  27393  tgjustc1  27726  tgjustc2  27727  tgbtwnconn1lem3  27825  legtrid  27842  tglinethru  27887  tglnpt2  27892  tglineintmo  27893  mirreu3  27905  perpcom  27964  footexALT  27969  footex  27972  mideu  27989  opphllem1  27998  lnopp2hpgb  28014  axsegcon  28185  axpasch  28199  axeuclidlem  28220  ecgrtg  28241  elntg  28242  eengtrkg  28244  upgr1eopALT  28377  usgredg4  28474  usgr1eop  28507  usgr1v  28513  subuhgr  28543  subumgr  28545  subusgr  28546  nbuhgr2vtx1edgb  28609  wwlksnext  29147  usgr2wspthon  29219  clwlkclwwlkf1  29263  clwwisshclwwslem  29267  n4cyclfrgr  29544  dlwwlknondlwlknonf1o  29618  vacn  29947  ubthlem1  30123  ubthlem3  30125  minvecolem7  30136  chocunii  30554  pjhthmo  30555  pjhthlem2  30645  nmopub2tALT  31162  nmfnleub2  31179  kbass5  31373  mdslmd1lem1  31578  mdslmd1lem2  31579  mdsymlem5  31660  fcobij  31947  xrofsup  31980  mgcf1o  32173  xrge0tsmsd  32209  symgcntz  32246  archiabllem2a  32340  gsumvsca1  32371  gsumvsca2  32372  isarchiofld  32435  prmidl2  32559  ssmxidl  32590  smatrcl  32776  reff  32819  ordtconnlem1  32904  qqhval2  32962  esumpcvgval  33076  imambfm  33261  ballotlemsf1o  33512  signstfvneq0  33583  pconnconn  34222  connpconn  34226  cvmliftmo  34275  cvmlift2lem10  34303  cvmlift2lem12  34305  cvmlift3lem7  34316  mrsubff1  34505  msubff1  34547  ifscgr  35016  cgrxfr  35027  btwnconn1lem13  35071  ellines  35124  unblimceq0lem  35382  unbdqndv2  35387  irrdiff  36207  matunitlindflem1  36484  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  heicant  36523  opnmbllem0  36524  mblfinlem3  36527  itg2addnclem  36539  itg2addnc  36542  ftc1cnnc  36560  sstotbnd  36643  cntotbnd  36664  ismtyima  36671  heibor1lem  36677  heiborlem10  36688  bfp  36692  rrncmslem  36700  islshpsm  37850  lsatcmp  37873  islshpat  37887  lfl0f  37939  iscvlat2N  38194  ishlat3N  38224  3dim1  38338  islvol5  38450  lvoli2  38452  lncvrelatN  38652  lncmp  38654  paddasslem10  38700  pclfinclN  38821  pexmidlem8N  38848  idltrn  39021  cdleme42keg  39357  cdleme42mgN  39359  cdlemf2  39433  cdlemg2cex  39462  trlcoat  39594  tendoex  39846  erngdvlem4  39862  erngdvlem4-rN  39870  dialss  39917  dibglbN  40037  diblss  40041  dihlsscpre  40105  dihglblem2aN  40164  dihglblem4  40168  dihglblem5  40169  dih1dimatlem  40200  dihglblem6  40211  lcfl7N  40372  lcfrlem9  40421  mapdh9a  40660  hdmapglem7  40800  aks4d1p8  40952  sticksstones22  40984  imacrhmcl  41089  fsuppind  41162  renegeulemv  41241  sn-subeu  41299  remulinvcom  41305  itrere  41339  retire  41340  prjspertr  41347  prjspreln0  41351  flt4lem7  41401  nna4b4nsq  41402  isnacs3  41448  nacsfix  41450  mzpsubst  41486  eldioph2lem2  41499  eldioph2  41500  eldioph2b  41501  diophin  41510  diophun  41511  rencldnfilem  41558  irrapxlem3  41562  irrapxlem5  41564  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell1qrge1  41608  pell1qrgaplem  41611  monotuz  41680  monotoddzzfi  41681  acongtr  41717  acongrep  41719  jm2.26a  41739  jm2.26lem3  41740  jm2.26  41741  jm2.27b  41745  jm2.27  41747  wepwsolem  41784  fnwe2lem2  41793  hbtlem5  41870  hbt  41872  mpaaeu  41892  cantnftermord  42070  cantnfresb  42074  omabs2  42082  tfsconcatun  42087  tfsconcatfn  42088  tfsconcatfv1  42089  tfsconcatfv2  42090  tfsconcatfv  42091  tfsconcatrn  42092  naddcnff  42112  oaun3lem1  42124  rfovcnvf1od  42755  mnurndlem1  43040  fnchoice  43713  rfcnnnub  43720  disjxp1  43756  ioondisj2  44206  iccintsng  44236  fprodcn  44316  lptioo2  44347  lptioo1  44348  limclner  44367  dvdsn1add  44655  stoweidlem14  44730  stoweidlem27  44743  stoweidlem34  44750  stoweidlem49  44765  stoweidlem56  44772  fourierdlem87  44909  iundjiun  45176  ismeannd  45183  hoidmvle  45316  prproropf1olem2  46172  perfectALTVlem2  46390  mogoldbb  46453  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  mgmhmeql  46573  rngpropd  46673  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  mndpsuppss  47047  lindslinindsimp2lem5  47143  itscnhlinecirc02p  47471  toslat  47607  functhinclem4  47664