Theorem simplr1 1215

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 726	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  6168  frfi  9349  wemappo  9618  iccsplit  13545  ccatswrd  14716  sqrmo  15300  pcdvdstr  16923  vdwlem12  17039  mreexexlem4d  17705  iscatd2  17739  oppccomfpropd  17787  resssetc  18159  resscatc  18176  mod1ile  18563  mod2ile  18564  prdssgrpd  18771  prdsmndd  18805  grprcan  19013  prdsrngd  20203  prdsringd  20344  lmodprop2d  20944  lssintcl  20985  prdslmodd  20990  islmhm2  21060  islbs3  21180  ofco2  22478  mdetmul  22650  restopnb  23204  regsep2  23405  iunconn  23457  blsscls2  24538  met2ndci  24556  xrsblre  24852  nosupbnd1lem5  27775  conway  27862  addsass  28056  mulscom  28183  legso  28625  colline  28675  tglowdim2ln  28677  cgrahl  28853  f1otrg  28897  f1otrge  28898  ax5seglem4  28965  ax5seglem5  28966  axcontlem4  29000  axcontlem8  29004  axcontlem9  29005  axcontlem10  29006  eengtrkg  29019  rusgrnumwwlks  30007  frgr3v  30307  lmhmimasvsca  33025  submomnd  33060  ogrpaddltbi  33068  erdszelem8  35166  elmrsubrn  35488  btwncomim  35977  btwnswapid  35981  broutsideof3  36090  outsideoftr  36093  outsidele  36096  isbasisrelowllem1  37321  isbasisrelowllem2  37322  cvrletrN  39229  ltltncvr  39380  atcvrj2b  39389  2at0mat0  39482  paddasslem11  39787  pmod1i  39805  lautcvr  40049  tendoplass  40740  tendodi1  40741  tendodi2  40742  cdlemk34  40867  mendassa  43151  grumnud  44255  3adantlr3  44940  ssinc  44989  ssdec  44990  ioondisj2  45411  ioondisj1  45412  subsubelfzo0  47241  ply1mulgsumlem2  48116  lincresunit3lem2  48209  catprs  48678