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

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

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 1088

This theorem is referenced by:  soltmin  6089  frfi  9190  wemappo  9460  iccsplit  13406  ccatswrd  14593  sqrmo  15176  pcdvdstr  16806  vdwlem12  16922  mreexexlem4d  17571  iscatd2  17605  oppccomfpropd  17651  resssetc  18017  resscatc  18034  mod1ile  18417  mod2ile  18418  prdssgrpd  18625  prdsmndd  18662  grprcan  18870  submomnd  20029  ogrpaddltbi  20036  prdsrngd  20079  prdsringd  20224  lmodprop2d  20845  lssintcl  20885  prdslmodd  20890  islmhm2  20960  islbs3  21080  ofco2  22354  mdetmul  22526  restopnb  23078  regsep2  23279  iunconn  23331  blsscls2  24408  met2ndci  24426  xrsblre  24716  nosupbnd1lem5  27640  conway  27728  addsass  27935  mulscom  28065  legso  28562  colline  28612  tglowdim2ln  28614  cgrahl  28790  f1otrg  28834  f1otrge  28835  ax5seglem4  28895  ax5seglem5  28896  axcontlem4  28930  axcontlem8  28934  axcontlem9  28935  axcontlem10  28936  eengtrkg  28949  rusgrnumwwlks  29937  frgr3v  30237  lmhmimasvsca  33006  erdszelem8  35173  elmrsubrn  35495  btwncomim  35989  btwnswapid  35993  broutsideof3  36102  outsideoftr  36105  outsidele  36108  isbasisrelowllem1  37331  isbasisrelowllem2  37332  cvrletrN  39254  ltltncvr  39405  atcvrj2b  39414  2at0mat0  39507  paddasslem11  39812  pmod1i  39830  lautcvr  40074  tendoplass  40765  tendodi1  40766  tendodi2  40767  cdlemk34  40892  mendassa  43166  grumnud  44262  3adantlr3  45021  ssinc  45068  ssdec  45069  ioondisj2  45478  ioondisj1  45479  subsubelfzo0  47314  ply1mulgsumlem2  48376  lincresunit3lem2  48469  catprs  49000  fthcomf  49146  oppcthinco  49428  oppcthinendcALT  49430