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  6093  frfi  9185  wemappo  9454  iccsplit  13401  ccatswrd  14592  sqrmo  15174  pcdvdstr  16804  vdwlem12  16920  mreexexlem4d  17570  iscatd2  17604  oppccomfpropd  17650  resssetc  18016  resscatc  18033  mod1ile  18416  mod2ile  18417  prdssgrpd  18658  prdsmndd  18695  grprcan  18903  submomnd  20061  ogrpaddltbi  20068  prdsrngd  20111  prdsringd  20256  lmodprop2d  20875  lssintcl  20915  prdslmodd  20920  islmhm2  20990  islbs3  21110  ofco2  22395  mdetmul  22567  restopnb  23119  regsep2  23320  iunconn  23372  blsscls2  24448  met2ndci  24466  xrsblre  24756  nosupbnd1lem5  27680  conway  27775  addsass  28001  mulscom  28135  legso  28671  colline  28721  tglowdim2ln  28723  cgrahl  28899  f1otrg  28943  f1otrge  28944  ax5seglem4  29005  ax5seglem5  29006  axcontlem4  29040  axcontlem8  29044  axcontlem9  29045  axcontlem10  29046  eengtrkg  29059  rusgrnumwwlks  30050  frgr3v  30350  lmhmimasvsca  33121  erdszelem8  35392  elmrsubrn  35714  btwncomim  36207  btwnswapid  36211  broutsideof3  36320  outsideoftr  36323  outsidele  36326  isbasisrelowllem1  37556  isbasisrelowllem2  37557  cvrletrN  39529  ltltncvr  39679  atcvrj2b  39688  2at0mat0  39781  paddasslem11  40086  pmod1i  40104  lautcvr  40348  tendoplass  41039  tendodi1  41040  tendodi2  41041  cdlemk34  41166  mendassa  43428  grumnud  44523  3adantlr3  45281  ssinc  45327  ssdec  45328  ioondisj2  45735  ioondisj1  45736  subsubelfzo0  47568  ply1mulgsumlem2  48629  lincresunit3lem2  48722  catprs  49252  fthcomf  49398  oppcthinco  49680  oppcthinendcALT  49682