Theorem simplr1 1216

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 726	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  soltmin  6135  frfi  9285  wemappo  9541  iccsplit  13459  ccatswrd  14615  sqrmo  15195  pcdvdstr  16806  vdwlem12  16922  mreexexlem4d  17588  iscatd2  17622  oppccomfpropd  17670  resssetc  18039  resscatc  18056  mod1ile  18443  mod2ile  18444  prdssgrpd  18621  prdsmndd  18655  grprcan  18855  prdsringd  20128  lmodprop2d  20527  lssintcl  20568  prdslmodd  20573  islmhm2  20642  islbs3  20761  ofco2  21945  mdetmul  22117  restopnb  22671  regsep2  22872  iunconn  22924  blsscls2  24005  met2ndci  24023  xrsblre  24319  nosupbnd1lem5  27205  conway  27290  addsass  27478  mulscom  27585  legso  27840  colline  27890  tglowdim2ln  27892  cgrahl  28068  f1otrg  28112  f1otrge  28113  ax5seglem4  28180  ax5seglem5  28181  axcontlem4  28215  axcontlem8  28219  axcontlem9  28220  axcontlem10  28221  eengtrkg  28234  rusgrnumwwlks  29218  frgr3v  29518  submomnd  32216  ogrpaddltbi  32224  erdszelem8  34178  elmrsubrn  34500  btwncomim  34974  btwnswapid  34978  broutsideof3  35087  outsideoftr  35090  outsidele  35093  isbasisrelowllem1  36225  isbasisrelowllem2  36226  cvrletrN  38132  ltltncvr  38283  atcvrj2b  38292  2at0mat0  38385  paddasslem11  38690  pmod1i  38708  lautcvr  38952  tendoplass  39643  tendodi1  39644  tendodi2  39645  cdlemk34  39770  mendassa  41922  grumnud  43031  3adantlr3  43710  ssinc  43762  ssdec  43763  ioondisj2  44193  ioondisj1  44194  subsubelfzo0  46021  prdsrngd  46664  ply1mulgsumlem2  47022  lincresunit3lem2  47115  catprs  47585