Theorem simplr1 1217

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

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

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 1089

This theorem is referenced by:  soltmin  6101  frfi  9197  wemappo  9466  iccsplit  13413  ccatswrd  14604  sqrmo  15186  pcdvdstr  16816  vdwlem12  16932  mreexexlem4d  17582  iscatd2  17616  oppccomfpropd  17662  resssetc  18028  resscatc  18045  mod1ile  18428  mod2ile  18429  prdssgrpd  18670  prdsmndd  18707  grprcan  18915  submomnd  20073  ogrpaddltbi  20080  prdsrngd  20123  prdsringd  20268  lmodprop2d  20887  lssintcl  20927  prdslmodd  20932  islmhm2  21002  islbs3  21122  ofco2  22407  mdetmul  22579  restopnb  23131  regsep2  23332  iunconn  23384  blsscls2  24460  met2ndci  24478  xrsblre  24768  nosupbnd1lem5  27692  conway  27787  addsass  28013  mulscom  28147  legso  28683  colline  28733  tglowdim2ln  28735  cgrahl  28911  f1otrg  28955  f1otrge  28956  ax5seglem4  29017  ax5seglem5  29018  axcontlem4  29052  axcontlem8  29056  axcontlem9  29057  axcontlem10  29058  eengtrkg  29071  rusgrnumwwlks  30062  frgr3v  30362  lmhmimasvsca  33131  erdszelem8  35411  elmrsubrn  35733  btwncomim  36226  btwnswapid  36230  broutsideof3  36339  outsideoftr  36342  outsidele  36345  isbasisrelowllem1  37607  isbasisrelowllem2  37608  cvrletrN  39646  ltltncvr  39796  atcvrj2b  39805  2at0mat0  39898  paddasslem11  40203  pmod1i  40221  lautcvr  40465  tendoplass  41156  tendodi1  41157  tendodi2  41158  cdlemk34  41283  mendassa  43544  grumnud  44639  3adantlr3  45397  ssinc  45443  ssdec  45444  ioondisj2  45850  ioondisj1  45851  subsubelfzo0  47683  ply1mulgsumlem2  48744  lincresunit3lem2  48837  catprs  49367  fthcomf  49513  oppcthinco  49795  oppcthinendcALT  49797