Theorem simplr1 1123

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

Assertion

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

Proof of Theorem simplr1

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

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

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

This theorem is referenced by:  soltmin  5567  frfi  8246  wemappo  8495  iccsplit  12343  ccatswrd  13502  sqrmo  14036  pcdvdstr  15627  vdwlem12  15743  mreexexlem4d  16354  iscatd2  16389  oppccomfpropd  16434  resssetc  16789  resscatc  16802  mod1ile  17152  mod2ile  17153  prdsmndd  17370  grprcan  17502  prdsringd  18658  lmodprop2d  18973  lssintcl  19012  prdslmodd  19017  islmhm2  19086  islbs3  19203  ofco2  20305  mdetmul  20477  restopnb  21027  regsep2  21228  iunconn  21279  blsscls2  22356  met2ndci  22374  xrsblre  22661  legso  25539  colline  25589  tglowdim2ln  25591  cgrahl  25763  f1otrg  25796  f1otrge  25797  ax5seglem4  25857  ax5seglem5  25858  axcontlem4  25892  axcontlem8  25896  axcontlem9  25897  axcontlem10  25898  eengtrkg  25910  rusgrnumwwlks  26941  frgr3v  27255  submomnd  29838  ogrpaddltbi  29847  erdszelem8  31306  nosupbnd1lem5  31983  conway  32035  btwncomim  32245  btwnswapid  32249  broutsideof3  32358  outsideoftr  32361  outsidele  32364  isbasisrelowllem1  33333  isbasisrelowllem2  33334  cvrletrN  34878  ltltncvr  35027  atcvrj2b  35036  2at0mat0  35129  paddasslem11  35434  pmod1i  35452  lautcvr  35696  tendoplass  36388  tendodi1  36389  tendodi2  36390  cdlemk34  36515  mendassa  38081  3adantlr3  39514  ssinc  39578  ssdec  39579  ioondisj2  40032  ioondisj1  40033  subsubelfzo0  41661  ply1mulgsumlem2  42500  lincresunit3lem2  42594