Theorem simplr1 1217

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

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

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 1091

This theorem is referenced by:  soltmin  6001  frfi  8916  wemappo  9165  iccsplit  13073  ccatswrd  14233  sqrmo  14815  pcdvdstr  16429  vdwlem12  16545  mreexexlem4d  17150  iscatd2  17184  oppccomfpropd  17231  resssetc  17598  resscatc  17615  mod1ile  17999  mod2ile  18000  prdsmndd  18206  grprcan  18401  prdsringd  19630  lmodprop2d  19961  lssintcl  20001  prdslmodd  20006  islmhm2  20075  islbs3  20192  ofco2  21348  mdetmul  21520  restopnb  22072  regsep2  22273  iunconn  22325  blsscls2  23402  met2ndci  23420  xrsblre  23708  legso  26690  colline  26740  tglowdim2ln  26742  cgrahl  26918  f1otrg  26962  f1otrge  26963  ax5seglem4  27023  ax5seglem5  27024  axcontlem4  27058  axcontlem8  27062  axcontlem9  27063  axcontlem10  27064  eengtrkg  27077  rusgrnumwwlks  28058  frgr3v  28358  submomnd  31055  ogrpaddltbi  31063  erdszelem8  32873  elmrsubrn  33195  nosupbnd1lem5  33652  conway  33730  btwncomim  34052  btwnswapid  34056  broutsideof3  34165  outsideoftr  34168  outsidele  34171  isbasisrelowllem1  35263  isbasisrelowllem2  35264  cvrletrN  37024  ltltncvr  37174  atcvrj2b  37183  2at0mat0  37276  paddasslem11  37581  pmod1i  37599  lautcvr  37843  tendoplass  38534  tendodi1  38535  tendodi2  38536  cdlemk34  38661  mendassa  40722  grumnud  41577  3adantlr3  42257  ssinc  42310  ssdec  42311  ioondisj2  42706  ioondisj1  42707  subsubelfzo0  44491  ply1mulgsumlem2  45401  lincresunit3lem2  45494  catprs  45965