Theorem simplr1 1216

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  6087  frfi  9176  wemappo  9442  iccsplit  13387  ccatswrd  14578  sqrmo  15160  pcdvdstr  16790  vdwlem12  16906  mreexexlem4d  17555  iscatd2  17589  oppccomfpropd  17635  resssetc  18001  resscatc  18018  mod1ile  18401  mod2ile  18402  prdssgrpd  18643  prdsmndd  18680  grprcan  18888  submomnd  20046  ogrpaddltbi  20053  prdsrngd  20096  prdsringd  20241  lmodprop2d  20859  lssintcl  20899  prdslmodd  20904  islmhm2  20974  islbs3  21094  ofco2  22367  mdetmul  22539  restopnb  23091  regsep2  23292  iunconn  23344  blsscls2  24420  met2ndci  24438  xrsblre  24728  nosupbnd1lem5  27652  conway  27741  addsass  27949  mulscom  28079  legso  28578  colline  28628  tglowdim2ln  28630  cgrahl  28806  f1otrg  28850  f1otrge  28851  ax5seglem4  28912  ax5seglem5  28913  axcontlem4  28947  axcontlem8  28951  axcontlem9  28952  axcontlem10  28953  eengtrkg  28966  rusgrnumwwlks  29957  frgr3v  30257  lmhmimasvsca  33027  erdszelem8  35263  elmrsubrn  35585  btwncomim  36078  btwnswapid  36082  broutsideof3  36191  outsideoftr  36194  outsidele  36197  isbasisrelowllem1  37420  isbasisrelowllem2  37421  cvrletrN  39393  ltltncvr  39543  atcvrj2b  39552  2at0mat0  39645  paddasslem11  39950  pmod1i  39968  lautcvr  40212  tendoplass  40903  tendodi1  40904  tendodi2  40905  cdlemk34  41030  mendassa  43308  grumnud  44404  3adantlr3  45162  ssinc  45209  ssdec  45210  ioondisj2  45618  ioondisj1  45619  subsubelfzo0  47451  ply1mulgsumlem2  48513  lincresunit3lem2  48606  catprs  49137  fthcomf  49283  oppcthinco  49565  oppcthinendcALT  49567