Theorem simplr2 1217

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr2	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simp2 1137	. 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  6089  frfi  9190  wemappo  9460  iccsplit  13406  ccatswrd  14593  pcdvdstr  16806  vdwlem12  16922  iscatd2  17605  oppccomfpropd  17651  resssetc  18017  resscatc  18034  mod1ile  18417  mod2ile  18418  prdssgrpd  18625  prdsmndd  18662  grprcan  18870  mulgnn0dir  19001  mulgnn0di  19722  mulgdi  19723  submomnd  20029  ogrpaddltbi  20036  lmodprop2d  20845  lssintcl  20885  prdslmodd  20890  islmhm2  20960  islbs3  21080  mdetmul  22526  restopnb  23078  nrmsep  23260  iunconn  23331  ptpjopn  23515  blsscls2  24408  xrsblre  24716  icccmplem2  24728  icccvx  24864  conway  27728  addsass  27935  mulscom  28065  colline  28612  tglowdim2ln  28614  f1otrg  28834  f1otrge  28835  ax5seglem5  28896  axcontlem3  28929  axcontlem4  28930  axcontlem8  28934  eengtrkg  28949  2pthon3v  29906  erclwwlktr  29984  erclwwlkntr  30033  eucrctshift  30205  frgr3v  30237  frgr2wwlkeqm  30293  xrofsup  32723  lmhmimasvsca  33006  erdszelem8  35170  cvmliftmolem2  35254  cvmlift2lem12  35286  r1peuqusdeg1  35615  btwnswapid  35990  btwnsegle  36090  broutsideof3  36099  outsidele  36105  isbasisrelowllem2  37329  cvrletrN  39251  ltltncvr  39402  atcvrj2b  39411  cvrat4  39422  2at0mat0  39504  islpln2a  39527  paddasslem11  39809  pmod1i  39827  lautcvr  40071  cdlemg4c  40591  tendoplass  40762  tendodi1  40763  tendodi2  40764  mendlmod  43162  mendassa  43163  3adantlr3  45018  ssinc  45065  ssdec  45066  ioondisj2  45475  ioondisj1  45476  stoweidlem60  46042  ply1mulgsumlem2  48373  lincresunit3lem2  48466  catprs  48997  fthcomf  49143  oppcthinco  49425  oppcthinendcALT  49427