Theorem simplr1 1233

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  soltmin  6135  frfi  9243  wemappo  9509  iccsplit  13518  ccatswrd  14713  sqrmo  15309  pcdvdstr  16942  vdwlem12  17058  mreexexlem4d  17709  iscatd2  17743  oppccomfpropd  17789  resssetc  18155  resscatc  18172  mod1ile  18555  mod2ile  18556  prdssgrpd  18797  prdsmndd  18834  grprcan  19046  submomnd  20208  ogrpaddltbi  20215  prdsrngd  20260  prdsringd  20409  lmodprop2d  21056  lssintcl  21096  prdslmodd  21101  islmhm2  21170  islbs3  21290  ofco2  22619  mdetmul  22791  restopnb  23343  regsep2  23544  iunconn  23596  blsscls2  24672  met2ndci  24690  xrsblre  24980  nosupbnd1lem5  27887  conway  27983  addsass  28209  mulscom  28343  legso  28879  colline  28934  tglowdim2ln  28936  cgrahl  29149  f1otrg  29231  f1otrge  29232  ax5seglem4  29293  ax5seglem5  29294  axcontlem4  29328  axcontlem8  29332  axcontlem9  29333  axcontlem10  29334  eengtrkg  29347  rusgrnumwwlks  30337  frgr3v  30637  lmhmimasvsca  33367  erdszelem8  35698  elmrsubrn  36020  btwncomim  36513  btwnswapid  36517  broutsideof3  36626  outsideoftr  36629  outsidele  36632  nmulprop  36690  nmulcom  36694  isbasisrelowllem1  38029  isbasisrelowllem2  38030  cvrletrN  40075  ltltncvr  40225  atcvrj2b  40234  2at0mat0  40327  paddasslem11  40632  pmod1i  40650  lautcvr  40894  tendoplass  41585  tendodi1  41586  tendodi2  41587  cdlemk34  41712  mendassa  43945  grumnud  45024  3adantlr3  45788  ssinc  45833  ssdec  45834  ioondisj2  46237  ioondisj1  46238  subsubelfzo0  48092  ply1mulgsumlem2  49195  lincresunit3lem2  49288  catprs  49817  fthcomf  49963  oppcthinco  50245  oppcthinendcALT  50247