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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6129  frfi  9279  wemappo  9546  iccsplit  13619  ccatswrd  14822  sqrmo  15423  pcdvdstr  17059  vdwlem12  17175  mreexexlem4d  17826  iscatd2  17860  oppccomfpropd  17906  resssetc  18272  resscatc  18289  mod1ile  18672  mod2ile  18673  prdssgrpd  18927  prdsmndd  18969  grprcan  19189  submomnd  20351  ogrpaddltbi  20358  prdsrngd  20403  prdsringd  20555  lmodprop2d  21204  lssintcl  21244  prdslmodd  21249  islmhm2  21318  islbs3  21438  ofco2  22771  mdetmul  22943  restopnb  23498  regsep2  23699  iunconn  23751  blsscls2  24828  met2ndci  24846  xrsblre  25136  nosupbnd1lem5  28074  conway  28170  addsass  28396  mulscom  28530  legso  29067  colline  29123  tglowdim2ln  29125  cgrahl  29340  f1otrg  29453  f1otrge  29454  ax5seglem4  29515  ax5seglem5  29516  axcontlem4  29550  axcontlem8  29554  axcontlem9  29555  axcontlem10  29556  eengtrkg  29569  rusgrnumwwlks  30571  frgr3v  30881  lmhmimasvsca  33645  erdszelem8  36049  elmrsubrn  36371  btwncomim  36870  btwnswapid  36874  broutsideof3  36983  outsideoftr  36986  outsidele  36989  nmulprop  37031  nmulcom  37035  isbasisrelowllem1  38371  isbasisrelowllem2  38372  cvrletrN  40423  ltltncvr  40573  atcvrj2b  40582  2at0mat0  40675  paddasslem11  40980  pmod1i  40998  lautcvr  41242  tendoplass  41933  tendodi1  41934  tendodi2  41935  cdlemk34  42060  mendassa  44285  grumnud  45363  3adantlr3  46150  ssinc  46195  ssdec  46196  ioondisj2  46598  ioondisj1  46599  tmachlem-franscan  48052  subsubelfzo0  48490  ply1mulgsumlem2  49592  lincresunit3lem2  49685  catprs  50218  fthcomf  50366  oppcthinco  50667  oppcthinendcALT  50669