Theorem simplr2 1097

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simplr2	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simpr2 1061	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	adantr 480	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  soltmin  5451  frfi  8090  wemappo  8337  iccsplit  12176  ccatswrd  13308  pcdvdstr  15418  vdwlem12  15534  iscatd2  16165  oppccomfpropd  16210  resssetc  16565  resscatc  16578  mod1ile  16928  mod2ile  16929  prdsmndd  17146  grprcan  17278  mulgnn0dir  17394  mulgnn0di  18054  mulgdi  18055  lmodprop2d  18748  lssintcl  18785  prdslmodd  18790  islmhm2  18859  islbs3  18976  mdetmul  20248  restopnb  20789  nrmsep  20971  iuncon  21041  ptpjopn  21225  blsscls2  22119  xrsblre  22422  icccmplem2  22434  icccvx  22557  colline  25344  tglowdim2ln  25346  f1otrg  25551  f1otrge  25552  ax5seglem5  25613  axcontlem3  25646  axcontlem4  25647  axcontlem8  25651  eengtrkg  25665  erclwwlktr  26343  erclwwlkntr  26355  el2wlkonotot0  26399  extwwlkfablem1  26601  xrofsup  28923  submomnd  29041  ogrpaddltbi  29050  erdszelem8  30434  cvmliftmolem2  30518  cvmlift2lem12  30550  btwnswapid  31294  btwnsegle  31394  broutsideof3  31403  outsidele  31409  isbasisrelowllem2  32380  cvrletrN  33578  ltltncvr  33727  atcvrj2b  33736  cvrat4  33747  2at0mat0  33829  islpln2a  33852  paddasslem11  34134  pmod1i  34152  lautcvr  34396  cdlemg4c  34918  tendoplass  35089  tendodi1  35090  tendodi2  35091  mendlmod  36782  mendassa  36783  3adantlr3  38223  ssinc  38292  ssdec  38293  ioondisj2  38561  ioondisj1  38562  stoweidlem60  38953  2pthon3v-av  41150  erclwwlkstr  41243  erclwwlksntr  41255  eucrctshift  41411  frgr3v  41445  ply1mulgsumlem2  41969  lincresunit3lem2  42063