Theorem simplr1 1228

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soltmin  6120  frfi  9225  wemappo  9494  iccsplit  13486  ccatswrd  14679  sqrmo  15261  pcdvdstr  16895  vdwlem12  17011  mreexexlem4d  17662  iscatd2  17696  oppccomfpropd  17742  resssetc  18108  resscatc  18125  mod1ile  18508  mod2ile  18509  prdssgrpd  18750  prdsmndd  18787  grprcan  18998  submomnd  20155  ogrpaddltbi  20162  prdsrngd  20205  prdsringd  20348  lmodprop2d  20971  lssintcl  21011  prdslmodd  21016  islmhm2  21085  islbs3  21205  ofco2  22491  mdetmul  22663  restopnb  23215  regsep2  23416  iunconn  23468  blsscls2  24544  met2ndci  24562  xrsblre  24852  nosupbnd1lem5  27753  conway  27849  addsass  28075  mulscom  28209  legso  28745  colline  28795  tglowdim2ln  28797  cgrahl  28973  f1otrg  29017  f1otrge  29018  ax5seglem4  29079  ax5seglem5  29080  axcontlem4  29114  axcontlem8  29118  axcontlem9  29119  axcontlem10  29120  eengtrkg  29133  rusgrnumwwlks  30123  frgr3v  30423  lmhmimasvsca  33178  erdszelem8  35512  elmrsubrn  35834  btwncomim  36327  btwnswapid  36331  broutsideof3  36440  outsideoftr  36443  outsidele  36446  nmulprop  36504  nmulcom  36508  isbasisrelowllem1  37813  isbasisrelowllem2  37814  cvrletrN  39861  ltltncvr  40011  atcvrj2b  40020  2at0mat0  40113  paddasslem11  40418  pmod1i  40436  lautcvr  40680  tendoplass  41371  tendodi1  41372  tendodi2  41373  cdlemk34  41498  mendassa  43731  grumnud  44826  3adantlr3  45584  ssinc  45629  ssdec  45630  ioondisj2  46033  ioondisj1  46034  subsubelfzo0  47885  ply1mulgsumlem2  48973  lincresunit3lem2  49066  catprs  49596  fthcomf  49742  oppcthinco  50024  oppcthinendcALT  50026