Theorem simplr1 1212

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  soltmin  5963  frfi  8747  wemappo  8997  iccsplit  12863  ccatswrd  14021  sqrmo  14603  pcdvdstr  16202  vdwlem12  16318  mreexexlem4d  16910  iscatd2  16944  oppccomfpropd  16989  resssetc  17344  resscatc  17357  mod1ile  17707  mod2ile  17708  prdsmndd  17936  grprcan  18129  prdsringd  19358  lmodprop2d  19689  lssintcl  19729  prdslmodd  19734  islmhm2  19803  islbs3  19920  ofco2  21056  mdetmul  21228  restopnb  21780  regsep2  21981  iunconn  22033  blsscls2  23111  met2ndci  23129  xrsblre  23416  legso  26393  colline  26443  tglowdim2ln  26445  cgrahl  26621  f1otrg  26665  f1otrge  26666  ax5seglem4  26726  ax5seglem5  26727  axcontlem4  26761  axcontlem8  26765  axcontlem9  26766  axcontlem10  26767  eengtrkg  26780  rusgrnumwwlks  27760  frgr3v  28060  submomnd  30761  ogrpaddltbi  30769  erdszelem8  32558  elmrsubrn  32880  nosupbnd1lem5  33325  conway  33377  btwncomim  33587  btwnswapid  33591  broutsideof3  33700  outsideoftr  33703  outsidele  33706  isbasisrelowllem1  34772  isbasisrelowllem2  34773  cvrletrN  36569  ltltncvr  36719  atcvrj2b  36728  2at0mat0  36821  paddasslem11  37126  pmod1i  37144  lautcvr  37388  tendoplass  38079  tendodi1  38080  tendodi2  38081  cdlemk34  38206  mendassa  40138  grumnud  40994  3adantlr3  41670  ssinc  41723  ssdec  41724  ioondisj2  42130  ioondisj1  42131  subsubelfzo0  43883  ply1mulgsumlem2  44795  lincresunit3lem2  44889