Theorem simplr1 1215

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soltmin  6155  frfi  9322  wemappo  9590  iccsplit  13526  ccatswrd  14707  sqrmo  15291  pcdvdstr  16915  vdwlem12  17031  mreexexlem4d  17691  iscatd2  17725  oppccomfpropd  17771  resssetc  18138  resscatc  18155  mod1ile  18539  mod2ile  18540  prdssgrpd  18747  prdsmndd  18784  grprcan  18992  prdsrngd  20174  prdsringd  20319  lmodprop2d  20923  lssintcl  20963  prdslmodd  20968  islmhm2  21038  islbs3  21158  ofco2  22458  mdetmul  22630  restopnb  23184  regsep2  23385  iunconn  23437  blsscls2  24518  met2ndci  24536  xrsblre  24834  nosupbnd1lem5  27758  conway  27845  addsass  28039  mulscom  28166  legso  28608  colline  28658  tglowdim2ln  28660  cgrahl  28836  f1otrg  28880  f1otrge  28881  ax5seglem4  28948  ax5seglem5  28949  axcontlem4  28983  axcontlem8  28987  axcontlem9  28988  axcontlem10  28989  eengtrkg  29002  rusgrnumwwlks  29995  frgr3v  30295  lmhmimasvsca  33045  submomnd  33088  ogrpaddltbi  33096  erdszelem8  35204  elmrsubrn  35526  btwncomim  36015  btwnswapid  36019  broutsideof3  36128  outsideoftr  36131  outsidele  36134  isbasisrelowllem1  37357  isbasisrelowllem2  37358  cvrletrN  39275  ltltncvr  39426  atcvrj2b  39435  2at0mat0  39528  paddasslem11  39833  pmod1i  39851  lautcvr  40095  tendoplass  40786  tendodi1  40787  tendodi2  40788  cdlemk34  40913  mendassa  43207  grumnud  44310  3adantlr3  45050  ssinc  45097  ssdec  45098  ioondisj2  45511  ioondisj1  45512  subsubelfzo0  47343  ply1mulgsumlem2  48309  lincresunit3lem2  48402  catprs  48915  oppcthinco  49113  oppcthinendcALT  49115