Theorem simplr1 1096

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

Assertion

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

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simpr1 1060	. 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  sqrmo  13840  pcdvdstr  15418  vdwlem12  15534  mreexexlem4d  16130  iscatd2  16165  oppccomfpropd  16210  resssetc  16565  resscatc  16578  mod1ile  16928  mod2ile  16929  prdsmndd  17146  grprcan  17278  prdsringd  18435  lmodprop2d  18748  lssintcl  18785  prdslmodd  18790  islmhm2  18859  islbs3  18976  ofco2  20076  mdetmul  20248  restopnb  20789  regsep2  20990  iuncon  21041  blsscls2  22119  met2ndci  22137  xrsblre  22422  legso  25294  colline  25344  tglowdim2ln  25346  cgrahl  25518  f1otrg  25551  f1otrge  25552  ax5seglem4  25612  ax5seglem5  25613  axcontlem4  25647  axcontlem8  25651  axcontlem9  25652  axcontlem10  25653  eengtrkg  25665  el2wlksotot  26409  rusgranumwlks  26483  extwwlkfablem1  26601  submomnd  29041  ogrpaddltbi  29050  erdszelem8  30434  btwncomim  31290  btwnswapid  31294  broutsideof3  31403  outsideoftr  31406  outsidele  31409  isbasisrelowllem1  32379  isbasisrelowllem2  32380  cvrletrN  33578  ltltncvr  33727  atcvrj2b  33736  2at0mat0  33829  paddasslem11  34134  pmod1i  34152  lautcvr  34396  tendoplass  35089  tendodi1  35090  tendodi2  35091  cdlemk34  35216  mendassa  36783  3adantlr3  38223  ssinc  38292  ssdec  38293  ioondisj2  38561  ioondisj1  38562  subsubelfzo0  40359  rusgrnumwwlks  41177  frgr3v  41445  ply1mulgsumlem2  41969  lincresunit3lem2  42063