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  6134  frfi  9259  wemappo  9525  iccsplit  13542  ccatswrd  14742  sqrmo  15342  pcdvdstr  16974  vdwlem12  17090  mreexexlem4d  17741  iscatd2  17775  oppccomfpropd  17821  resssetc  18187  resscatc  18204  mod1ile  18587  mod2ile  18588  prdssgrpd  18841  prdsmndd  18883  grprcan  19103  submomnd  20265  ogrpaddltbi  20272  prdsrngd  20317  prdsringd  20467  lmodprop2d  21114  lssintcl  21154  prdslmodd  21159  islmhm2  21228  islbs3  21348  ofco2  22679  mdetmul  22851  restopnb  23406  regsep2  23607  iunconn  23659  blsscls2  24736  met2ndci  24754  xrsblre  25044  nosupbnd1lem5  27956  conway  28052  addsass  28278  mulscom  28412  legso  28949  colline  29005  tglowdim2ln  29007  cgrahl  29222  f1otrg  29335  f1otrge  29336  ax5seglem4  29397  ax5seglem5  29398  axcontlem4  29432  axcontlem8  29436  axcontlem9  29437  axcontlem10  29438  eengtrkg  29451  rusgrnumwwlks  30453  frgr3v  30763  lmhmimasvsca  33486  erdszelem8  35785  elmrsubrn  36107  btwncomim  36601  btwnswapid  36605  broutsideof3  36714  outsideoftr  36717  outsidele  36720  nmulprop  36778  nmulcom  36782  isbasisrelowllem1  38117  isbasisrelowllem2  38118  cvrletrN  40154  ltltncvr  40304  atcvrj2b  40313  2at0mat0  40406  paddasslem11  40711  pmod1i  40729  lautcvr  40973  tendoplass  41664  tendodi1  41665  tendodi2  41666  cdlemk34  41791  mendassa  44039  grumnud  45118  3adantlr3  45882  ssinc  45927  ssdec  45928  ioondisj2  46331  ioondisj1  46332  tmachlem-franscan  47785  subsubelfzo0  48223  ply1mulgsumlem2  49325  lincresunit3lem2  49418  catprs  49945  fthcomf  50091  oppcthinco  50373  oppcthinendcALT  50375