Theorem simplr2 1283

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  soltmin  5773  frfi  8473  wemappo  8722  iccsplit  12597  ccatswrd  13745  pcdvdstr  15950  vdwlem12  16066  iscatd2  16693  oppccomfpropd  16738  resssetc  17093  resscatc  17106  mod1ile  17457  mod2ile  17458  prdsmndd  17675  grprcan  17808  mulgnn0dir  17922  mulgnn0di  18583  mulgdi  18584  lmodprop2d  19280  lssintcl  19322  prdslmodd  19327  islmhm2  19396  islbs3  19515  mdetmul  20796  restopnb  21349  nrmsep  21531  iunconn  21601  ptpjopn  21785  blsscls2  22678  xrsblre  22983  icccmplem2  22995  icccvx  23118  colline  25960  tglowdim2ln  25962  f1otrg  26169  f1otrge  26170  ax5seglem5  26231  axcontlem3  26264  axcontlem4  26265  axcontlem8  26269  eengtrkg  26284  2pthon3v  27271  erclwwlktr  27359  erclwwlkntr  27423  eucrctshift  27619  frgr3v  27655  frgr2wwlkeqm  27711  xrofsup  30079  submomnd  30254  ogrpaddltbi  30263  erdszelem8  31725  cvmliftmolem2  31809  cvmlift2lem12  31841  conway  32448  btwnswapid  32662  btwnsegle  32762  broutsideof3  32771  outsidele  32777  isbasisrelowllem2  33748  cvrletrN  35347  ltltncvr  35497  atcvrj2b  35506  cvrat4  35517  2at0mat0  35599  islpln2a  35622  paddasslem11  35904  pmod1i  35922  lautcvr  36166  cdlemg4c  36686  tendoplass  36857  tendodi1  36858  tendodi2  36859  mendlmod  38605  mendassa  38606  3adantlr3  40017  ssinc  40080  ssdec  40081  ioondisj2  40512  ioondisj1  40513  stoweidlem60  41070  ply1mulgsumlem2  43021  lincresunit3lem2  43115