Theorem simplr1 1101

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

Assertion

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

Proof of Theorem simplr1

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

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

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 1038

This theorem is referenced by:  soltmin  5495  frfi  8150  wemappo  8399  iccsplit  12244  ccatswrd  13389  sqrmo  13921  pcdvdstr  15499  vdwlem12  15615  mreexexlem4d  16223  iscatd2  16258  oppccomfpropd  16303  resssetc  16658  resscatc  16671  mod1ile  17021  mod2ile  17022  prdsmndd  17239  grprcan  17371  prdsringd  18528  lmodprop2d  18841  lssintcl  18878  prdslmodd  18883  islmhm2  18952  islbs3  19069  ofco2  20171  mdetmul  20343  restopnb  20884  regsep2  21085  iunconn  21136  blsscls2  22214  met2ndci  22232  xrsblre  22517  legso  25389  colline  25439  tglowdim2ln  25441  cgrahl  25613  f1otrg  25646  f1otrge  25647  ax5seglem4  25707  ax5seglem5  25708  axcontlem4  25742  axcontlem8  25746  axcontlem9  25747  axcontlem10  25748  eengtrkg  25760  rusgrnumwwlks  26730  frgr3v  26997  submomnd  29487  ogrpaddltbi  29496  erdszelem8  30880  btwncomim  31754  btwnswapid  31758  broutsideof3  31867  outsideoftr  31870  outsidele  31873  isbasisrelowllem1  32827  isbasisrelowllem2  32828  cvrletrN  34026  ltltncvr  34175  atcvrj2b  34184  2at0mat0  34277  paddasslem11  34582  pmod1i  34600  lautcvr  34844  tendoplass  35537  tendodi1  35538  tendodi2  35539  cdlemk34  35664  mendassa  37231  3adantlr3  38669  ssinc  38735  ssdec  38736  ioondisj2  39112  ioondisj1  39113  subsubelfzo0  40621  ply1mulgsumlem2  41437  lincresunit3lem2  41531