Theorem simplr1 1217

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 728	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soltmin  6093  frfi  9188  wemappo  9457  iccsplit  13429  ccatswrd  14622  sqrmo  15204  pcdvdstr  16838  vdwlem12  16954  mreexexlem4d  17604  iscatd2  17638  oppccomfpropd  17684  resssetc  18050  resscatc  18067  mod1ile  18450  mod2ile  18451  prdssgrpd  18692  prdsmndd  18729  grprcan  18940  submomnd  20098  ogrpaddltbi  20105  prdsrngd  20148  prdsringd  20291  lmodprop2d  20910  lssintcl  20950  prdslmodd  20955  islmhm2  21025  islbs3  21145  ofco2  22426  mdetmul  22598  restopnb  23150  regsep2  23351  iunconn  23403  blsscls2  24479  met2ndci  24497  xrsblre  24787  nosupbnd1lem5  27690  conway  27785  addsass  28011  mulscom  28145  legso  28681  colline  28731  tglowdim2ln  28733  cgrahl  28909  f1otrg  28953  f1otrge  28954  ax5seglem4  29015  ax5seglem5  29016  axcontlem4  29050  axcontlem8  29054  axcontlem9  29055  axcontlem10  29056  eengtrkg  29069  rusgrnumwwlks  30060  frgr3v  30360  lmhmimasvsca  33114  erdszelem8  35396  elmrsubrn  35718  btwncomim  36211  btwnswapid  36215  broutsideof3  36324  outsideoftr  36327  outsidele  36330  isbasisrelowllem1  37685  isbasisrelowllem2  37686  cvrletrN  39733  ltltncvr  39883  atcvrj2b  39892  2at0mat0  39985  paddasslem11  40290  pmod1i  40308  lautcvr  40552  tendoplass  41243  tendodi1  41244  tendodi2  41245  cdlemk34  41370  mendassa  43636  grumnud  44731  3adantlr3  45489  ssinc  45535  ssdec  45536  ioondisj2  45941  ioondisj1  45942  subsubelfzo0  47787  ply1mulgsumlem2  48875  lincresunit3lem2  48968  catprs  49498  fthcomf  49644  oppcthinco  49926  oppcthinendcALT  49928