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  6090  frfi  9179  wemappo  9445  iccsplit  13395  ccatswrd  14586  sqrmo  15168  pcdvdstr  16798  vdwlem12  16914  mreexexlem4d  17563  iscatd2  17597  oppccomfpropd  17643  resssetc  18009  resscatc  18026  mod1ile  18409  mod2ile  18410  prdssgrpd  18651  prdsmndd  18688  grprcan  18896  submomnd  20054  ogrpaddltbi  20061  prdsrngd  20104  prdsringd  20249  lmodprop2d  20867  lssintcl  20907  prdslmodd  20912  islmhm2  20982  islbs3  21102  ofco2  22376  mdetmul  22548  restopnb  23100  regsep2  23301  iunconn  23353  blsscls2  24429  met2ndci  24447  xrsblre  24737  nosupbnd1lem5  27661  conway  27750  addsass  27958  mulscom  28088  legso  28587  colline  28637  tglowdim2ln  28639  cgrahl  28815  f1otrg  28859  f1otrge  28860  ax5seglem4  28921  ax5seglem5  28922  axcontlem4  28956  axcontlem8  28960  axcontlem9  28961  axcontlem10  28962  eengtrkg  28975  rusgrnumwwlks  29966  frgr3v  30266  lmhmimasvsca  33031  erdszelem8  35253  elmrsubrn  35575  btwncomim  36068  btwnswapid  36072  broutsideof3  36181  outsideoftr  36184  outsidele  36187  isbasisrelowllem1  37410  isbasisrelowllem2  37411  cvrletrN  39382  ltltncvr  39532  atcvrj2b  39541  2at0mat0  39634  paddasslem11  39939  pmod1i  39957  lautcvr  40201  tendoplass  40892  tendodi1  40893  tendodi2  40894  cdlemk34  41019  mendassa  43297  grumnud  44393  3adantlr3  45151  ssinc  45198  ssdec  45199  ioondisj2  45607  ioondisj1  45608  subsubelfzo0  47440  ply1mulgsumlem2  48502  lincresunit3lem2  48595  catprs  49126  fthcomf  49272  oppcthinco  49554  oppcthinendcALT  49556