Theorem simplr2 1104

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

Assertion

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

Proof of Theorem simplr2

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soltmin  5532  frfi  8205  wemappo  8454  iccsplit  12305  ccatswrd  13456  pcdvdstr  15580  vdwlem12  15696  iscatd2  16342  oppccomfpropd  16387  resssetc  16742  resscatc  16755  mod1ile  17105  mod2ile  17106  prdsmndd  17323  grprcan  17455  mulgnn0dir  17571  mulgnn0di  18231  mulgdi  18232  lmodprop2d  18925  lssintcl  18964  prdslmodd  18969  islmhm2  19038  islbs3  19155  mdetmul  20429  restopnb  20979  nrmsep  21161  iunconn  21231  ptpjopn  21415  blsscls2  22309  xrsblre  22614  icccmplem2  22626  icccvx  22749  colline  25544  tglowdim2ln  25546  f1otrg  25751  f1otrge  25752  ax5seglem5  25813  axcontlem3  25846  axcontlem4  25847  axcontlem8  25851  eengtrkg  25865  2pthon3v  26839  erclwwlkstr  26936  erclwwlksntr  26948  eucrctshift  27103  frgr3v  27139  frgr2wwlkeqm  27195  xrofsup  29533  submomnd  29710  ogrpaddltbi  29719  erdszelem8  31180  cvmliftmolem2  31264  cvmlift2lem12  31296  conway  31910  btwnswapid  32124  btwnsegle  32224  broutsideof3  32233  outsidele  32239  isbasisrelowllem2  33204  cvrletrN  34560  ltltncvr  34709  atcvrj2b  34718  cvrat4  34729  2at0mat0  34811  islpln2a  34834  paddasslem11  35116  pmod1i  35134  lautcvr  35378  cdlemg4c  35900  tendoplass  36071  tendodi1  36072  tendodi2  36073  mendlmod  37763  mendassa  37764  3adantlr3  39200  ssinc  39264  ssdec  39265  ioondisj2  39714  ioondisj1  39715  stoweidlem60  40277  ply1mulgsumlem2  42175  lincresunit3lem2  42269