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  6083  frfi  9169  wemappo  9435  iccsplit  13385  ccatswrd  14576  sqrmo  15158  pcdvdstr  16788  vdwlem12  16904  mreexexlem4d  17553  iscatd2  17587  oppccomfpropd  17633  resssetc  17999  resscatc  18016  mod1ile  18399  mod2ile  18400  prdssgrpd  18641  prdsmndd  18678  grprcan  18886  submomnd  20045  ogrpaddltbi  20052  prdsrngd  20095  prdsringd  20240  lmodprop2d  20858  lssintcl  20898  prdslmodd  20903  islmhm2  20973  islbs3  21093  ofco2  22367  mdetmul  22539  restopnb  23091  regsep2  23292  iunconn  23344  blsscls2  24420  met2ndci  24438  xrsblre  24728  nosupbnd1lem5  27652  conway  27741  addsass  27949  mulscom  28079  legso  28578  colline  28628  tglowdim2ln  28630  cgrahl  28806  f1otrg  28850  f1otrge  28851  ax5seglem4  28911  ax5seglem5  28912  axcontlem4  28946  axcontlem8  28950  axcontlem9  28951  axcontlem10  28952  eengtrkg  28965  rusgrnumwwlks  29953  frgr3v  30253  lmhmimasvsca  33018  erdszelem8  35240  elmrsubrn  35562  btwncomim  36053  btwnswapid  36057  broutsideof3  36166  outsideoftr  36169  outsidele  36172  isbasisrelowllem1  37395  isbasisrelowllem2  37396  cvrletrN  39318  ltltncvr  39468  atcvrj2b  39477  2at0mat0  39570  paddasslem11  39875  pmod1i  39893  lautcvr  40137  tendoplass  40828  tendodi1  40829  tendodi2  40830  cdlemk34  40955  mendassa  43229  grumnud  44325  3adantlr3  45083  ssinc  45130  ssdec  45131  ioondisj2  45539  ioondisj1  45540  subsubelfzo0  47363  ply1mulgsumlem2  48425  lincresunit3lem2  48518  catprs  49049  fthcomf  49195  oppcthinco  49477  oppcthinendcALT  49479