Theorem simplr2 1218

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 1138	. 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  pcdvdstr  16816  vdwlem12  16932  iscatd2  17616  oppccomfpropd  17662  resssetc  18028  resscatc  18045  mod1ile  18428  mod2ile  18429  prdssgrpd  18670  prdsmndd  18707  grprcan  18915  mulgnn0dir  19046  mulgnn0di  19766  mulgdi  19767  submomnd  20073  ogrpaddltbi  20080  lmodprop2d  20887  lssintcl  20927  prdslmodd  20932  islmhm2  21002  islbs3  21122  mdetmul  22579  restopnb  23131  nrmsep  23313  iunconn  23384  ptpjopn  23568  blsscls2  24460  xrsblre  24768  icccmplem2  24780  icccvx  24916  conway  27787  addsass  28013  mulscom  28147  addonbday  28287  colline  28733  tglowdim2ln  28735  f1otrg  28955  f1otrge  28956  ax5seglem5  29018  axcontlem3  29051  axcontlem4  29052  axcontlem8  29056  eengtrkg  29071  2pthon3v  30028  erclwwlktr  30109  erclwwlkntr  30158  eucrctshift  30330  frgr3v  30362  frgr2wwlkeqm  30418  xrofsup  32857  lmhmimasvsca  33131  erdszelem8  35411  cvmliftmolem2  35495  cvmlift2lem12  35527  r1peuqusdeg1  35856  btwnswapid  36230  btwnsegle  36330  broutsideof3  36339  outsidele  36345  isbasisrelowllem2  37605  cvrletrN  39643  ltltncvr  39793  atcvrj2b  39802  cvrat4  39813  2at0mat0  39895  islpln2a  39918  paddasslem11  40200  pmod1i  40218  lautcvr  40462  cdlemg4c  40982  tendoplass  41153  tendodi1  41154  tendodi2  41155  mendlmod  43540  mendassa  43541  3adantlr3  45394  ssinc  45440  ssdec  45441  ioondisj2  45847  ioondisj1  45848  stoweidlem60  46412  ply1mulgsumlem2  48741  lincresunit3lem2  48834  catprs  49364  fthcomf  49510  oppcthinco  49792  oppcthinendcALT  49794