Theorem simplr1 1234

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

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

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 1105

This theorem is referenced by:  soltmin  6138  frfi  9246  wemappo  9512  iccsplit  13513  ccatswrd  14708  sqrmo  15304  pcdvdstr  16937  vdwlem12  17053  mreexexlem4d  17704  iscatd2  17738  oppccomfpropd  17784  resssetc  18150  resscatc  18167  mod1ile  18550  mod2ile  18551  prdssgrpd  18792  prdsmndd  18829  grprcan  19041  submomnd  20203  ogrpaddltbi  20210  prdsrngd  20255  prdsringd  20403  lmodprop2d  21026  lssintcl  21066  prdslmodd  21071  islmhm2  21140  islbs3  21260  ofco2  22589  mdetmul  22761  restopnb  23313  regsep2  23514  iunconn  23566  blsscls2  24642  met2ndci  24660  xrsblre  24950  nosupbnd1lem5  27854  conway  27950  addsass  28176  mulscom  28310  legso  28846  colline  28901  tglowdim2ln  28903  cgrahl  29116  f1otrg  29198  f1otrge  29199  ax5seglem4  29260  ax5seglem5  29261  axcontlem4  29295  axcontlem8  29299  axcontlem9  29300  axcontlem10  29301  eengtrkg  29314  rusgrnumwwlks  30304  frgr3v  30604  lmhmimasvsca  33336  erdszelem8  35668  elmrsubrn  35990  btwncomim  36483  btwnswapid  36487  broutsideof3  36596  outsideoftr  36599  outsidele  36602  nmulprop  36660  nmulcom  36664  isbasisrelowllem1  37979  isbasisrelowllem2  37980  cvrletrN  40025  ltltncvr  40175  atcvrj2b  40184  2at0mat0  40277  paddasslem11  40582  pmod1i  40600  lautcvr  40844  tendoplass  41535  tendodi1  41536  tendodi2  41537  cdlemk34  41662  mendassa  43897  grumnud  44976  3adantlr3  45740  ssinc  45785  ssdec  45786  ioondisj2  46189  ioondisj1  46190  subsubelfzo0  48041  ply1mulgsumlem2  49144  lincresunit3lem2  49237  catprs  49766  fthcomf  49912  oppcthinco  50194  oppcthinendcALT  50196