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  6142  frfi  9304  wemappo  9570  iccsplit  13643  ccatswrd  14846  sqrmo  15447  pcdvdstr  17083  vdwlem12  17199  mreexexlem4d  17850  iscatd2  17884  oppccomfpropd  17930  resssetc  18296  resscatc  18313  mod1ile  18696  mod2ile  18697  prdssgrpd  18951  prdsmndd  18993  grprcan  19213  submomnd  20376  ogrpaddltbi  20383  prdsrngd  20428  prdsringd  20580  lmodprop2d  21229  lssintcl  21269  prdslmodd  21274  islmhm2  21343  islbs3  21463  ofco2  22796  mdetmul  22968  restopnb  23523  regsep2  23724  iunconn  23776  blsscls2  24853  met2ndci  24871  xrsblre  25161  nosupbnd1lem5  28099  conway  28195  addsass  28421  mulscom  28555  legso  29092  colline  29148  tglowdim2ln  29150  cgrahl  29365  f1otrg  29478  f1otrge  29479  ax5seglem4  29540  ax5seglem5  29541  axcontlem4  29575  axcontlem8  29579  axcontlem9  29580  axcontlem10  29581  eengtrkg  29594  rusgrnumwwlks  30596  frgr3v  30906  lmhmimasvsca  33669  erdszelem8  36130  elmrsubrn  36452  btwncomim  36956  btwnswapid  36960  broutsideof3  37069  outsideoftr  37072  outsidele  37075  nmulprop  37117  nmulcom  37121  isbasisrelowllem1  38470  isbasisrelowllem2  38471  cvrletrN  40522  ltltncvr  40672  atcvrj2b  40681  2at0mat0  40774  paddasslem11  41079  pmod1i  41097  lautcvr  41341  tendoplass  42032  tendodi1  42033  tendodi2  42034  cdlemk34  42159  mendassa  44384  grumnud  45462  3adantlr3  46262  ssinc  46307  ssdec  46308  ioondisj2  46710  ioondisj1  46711  tmachlem-franscan  48164  subsubelfzo0  48602  ply1mulgsumlem2  49704  lincresunit3lem2  49797  catprs  50330  fthcomf  50478  oppcthinco  50779  oppcthinendcALT  50781