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  6141  frfi  9255  wemappo  9521  iccsplit  13530  ccatswrd  14730  sqrmo  15328  pcdvdstr  16961  vdwlem12  17077  mreexexlem4d  17728  iscatd2  17762  oppccomfpropd  17808  resssetc  18174  resscatc  18191  mod1ile  18574  mod2ile  18575  prdssgrpd  18820  prdsmndd  18859  grprcan  19071  submomnd  20233  ogrpaddltbi  20240  prdsrngd  20285  prdsringd  20435  lmodprop2d  21082  lssintcl  21122  prdslmodd  21127  islmhm2  21196  islbs3  21316  ofco2  22645  mdetmul  22817  restopnb  23369  regsep2  23570  iunconn  23622  blsscls2  24698  met2ndci  24716  xrsblre  25006  nosupbnd1lem5  27913  conway  28009  addsass  28235  mulscom  28369  legso  28905  colline  28960  tglowdim2ln  28962  cgrahl  29175  f1otrg  29257  f1otrge  29258  ax5seglem4  29319  ax5seglem5  29320  axcontlem4  29354  axcontlem8  29358  axcontlem9  29359  axcontlem10  29360  eengtrkg  29373  rusgrnumwwlks  30363  frgr3v  30663  lmhmimasvsca  33389  erdszelem8  35711  elmrsubrn  36033  btwncomim  36526  btwnswapid  36530  broutsideof3  36639  outsideoftr  36642  outsidele  36645  nmulprop  36703  nmulcom  36707  isbasisrelowllem1  38042  isbasisrelowllem2  38043  cvrletrN  40088  ltltncvr  40238  atcvrj2b  40247  2at0mat0  40340  paddasslem11  40645  pmod1i  40663  lautcvr  40907  tendoplass  41598  tendodi1  41599  tendodi2  41600  cdlemk34  41725  mendassa  43958  grumnud  45037  3adantlr3  45801  ssinc  45846  ssdec  45847  ioondisj2  46250  ioondisj1  46251  subsubelfzo0  48105  ply1mulgsumlem2  49208  lincresunit3lem2  49301  catprs  49830  fthcomf  49976  oppcthinco  50258  oppcthinendcALT  50260