Theorem simplr1 1211

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simp1 1132	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 725	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soltmin  5996  frfi  8763  wemappo  9013  iccsplit  12872  ccatswrd  14030  sqrmo  14611  pcdvdstr  16212  vdwlem12  16328  mreexexlem4d  16918  iscatd2  16952  oppccomfpropd  16997  resssetc  17352  resscatc  17365  mod1ile  17715  mod2ile  17716  prdsmndd  17944  grprcan  18137  prdsringd  19362  lmodprop2d  19696  lssintcl  19736  prdslmodd  19741  islmhm2  19810  islbs3  19927  ofco2  21060  mdetmul  21232  restopnb  21783  regsep2  21984  iunconn  22036  blsscls2  23114  met2ndci  23132  xrsblre  23419  legso  26385  colline  26435  tglowdim2ln  26437  cgrahl  26613  f1otrg  26657  f1otrge  26658  ax5seglem4  26718  ax5seglem5  26719  axcontlem4  26753  axcontlem8  26757  axcontlem9  26758  axcontlem10  26759  eengtrkg  26772  rusgrnumwwlks  27753  frgr3v  28054  submomnd  30711  ogrpaddltbi  30719  erdszelem8  32445  elmrsubrn  32767  nosupbnd1lem5  33212  conway  33264  btwncomim  33474  btwnswapid  33478  broutsideof3  33587  outsideoftr  33590  outsidele  33593  isbasisrelowllem1  34639  isbasisrelowllem2  34640  cvrletrN  36424  ltltncvr  36574  atcvrj2b  36583  2at0mat0  36676  paddasslem11  36981  pmod1i  36999  lautcvr  37243  tendoplass  37934  tendodi1  37935  tendodi2  37936  cdlemk34  38061  mendassa  39814  grumnud  40642  3adantlr3  41318  ssinc  41373  ssdec  41374  ioondisj2  41787  ioondisj1  41788  subsubelfzo0  43546  ply1mulgsumlem2  44461  lincresunit3lem2  44555