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  6125  frfi  9293  wemappo  9563  iccsplit  13502  ccatswrd  14686  pcdvdstr  16896  vdwlem12  17012  iscatd2  17693  oppccomfpropd  17739  resssetc  18105  resscatc  18122  mod1ile  18503  mod2ile  18504  prdssgrpd  18711  prdsmndd  18748  grprcan  18956  mulgnn0dir  19087  mulgnn0di  19806  mulgdi  19807  lmodprop2d  20881  lssintcl  20921  prdslmodd  20926  islmhm2  20996  islbs3  21116  mdetmul  22561  restopnb  23113  nrmsep  23295  iunconn  23366  ptpjopn  23550  blsscls2  24443  xrsblre  24751  icccmplem2  24763  icccvx  24899  conway  27763  addsass  27964  mulscom  28094  colline  28628  tglowdim2ln  28630  f1otrg  28850  f1otrge  28851  ax5seglem5  28912  axcontlem3  28945  axcontlem4  28946  axcontlem8  28950  eengtrkg  28965  2pthon3v  29925  erclwwlktr  30003  erclwwlkntr  30052  eucrctshift  30224  frgr3v  30256  frgr2wwlkeqm  30312  xrofsup  32744  lmhmimasvsca  33034  submomnd  33078  ogrpaddltbi  33086  erdszelem8  35220  cvmliftmolem2  35304  cvmlift2lem12  35336  r1peuqusdeg1  35665  btwnswapid  36035  btwnsegle  36135  broutsideof3  36144  outsidele  36150  isbasisrelowllem2  37374  cvrletrN  39291  ltltncvr  39442  atcvrj2b  39451  cvrat4  39462  2at0mat0  39544  islpln2a  39567  paddasslem11  39849  pmod1i  39867  lautcvr  40111  cdlemg4c  40631  tendoplass  40802  tendodi1  40803  tendodi2  40804  mendlmod  43213  mendassa  43214  3adantlr3  45064  ssinc  45111  ssdec  45112  ioondisj2  45522  ioondisj1  45523  stoweidlem60  46089  ply1mulgsumlem2  48363  lincresunit3lem2  48456  catprs  48986  fthcomf  49097  oppcthinco  49325  oppcthinendcALT  49327