Theorem simplr1 1232

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  soltmin  6127  frfi  9233  wemappo  9499  iccsplit  13503  ccatswrd  14696  sqrmo  15292  pcdvdstr  16926  vdwlem12  17042  mreexexlem4d  17693  iscatd2  17727  oppccomfpropd  17773  resssetc  18139  resscatc  18156  mod1ile  18539  mod2ile  18540  prdssgrpd  18781  prdsmndd  18818  grprcan  19030  submomnd  20193  ogrpaddltbi  20200  prdsrngd  20245  prdsringd  20393  lmodprop2d  21014  lssintcl  21054  prdslmodd  21059  islmhm2  21128  islbs3  21248  ofco2  22569  mdetmul  22741  restopnb  23293  regsep2  23494  iunconn  23546  blsscls2  24622  met2ndci  24640  xrsblre  24930  nosupbnd1lem5  27834  conway  27930  addsass  28156  mulscom  28290  legso  28826  colline  28877  tglowdim2ln  28879  cgrahl  29079  f1otrg  29129  f1otrge  29130  ax5seglem4  29191  ax5seglem5  29192  axcontlem4  29226  axcontlem8  29230  axcontlem9  29231  axcontlem10  29232  eengtrkg  29245  rusgrnumwwlks  30235  frgr3v  30535  lmhmimasvsca  33271  erdszelem8  35561  elmrsubrn  35883  btwncomim  36376  btwnswapid  36380  broutsideof3  36489  outsideoftr  36492  outsidele  36495  nmulprop  36553  nmulcom  36557  isbasisrelowllem1  37861  isbasisrelowllem2  37862  cvrletrN  39909  ltltncvr  40059  atcvrj2b  40068  2at0mat0  40161  paddasslem11  40466  pmod1i  40484  lautcvr  40728  tendoplass  41419  tendodi1  41420  tendodi2  41421  cdlemk34  41546  mendassa  43779  grumnud  44860  3adantlr3  45618  ssinc  45663  ssdec  45664  ioondisj2  46067  ioondisj1  46068  subsubelfzo0  47919  ply1mulgsumlem2  49018  lincresunit3lem2  49111  catprs  49640  fthcomf  49786  oppcthinco  50068  oppcthinendcALT  50070