Theorem simplr2 1235

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6142  frfi  9304  wemappo  9570  iccsplit  13643  ccatswrd  14846  pcdvdstr  17083  vdwlem12  17199  iscatd2  17884  oppccomfpropd  17930  resssetc  18296  resscatc  18313  mod1ile  18696  mod2ile  18697  prdssgrpd  18951  prdsmndd  18993  grprcan  19213  mulgnn0dir  19343  mulgnn0di  20069  mulgdi  20070  submomnd  20376  ogrpaddltbi  20383  lmodprop2d  21229  lssintcl  21269  prdslmodd  21274  islmhm2  21343  islbs3  21463  mdetmul  22968  restopnb  23523  nrmsep  23705  iunconn  23776  ptpjopn  23961  blsscls2  24853  xrsblre  25161  icccmplem2  25173  icccvx  25301  conway  28195  addsass  28421  mulscom  28555  addonbday  28695  colline  29148  tglowdim2ln  29150  f1otrg  29478  f1otrge  29479  ax5seglem5  29541  axcontlem3  29574  axcontlem4  29575  axcontlem8  29579  eengtrkg  29594  2pthon3v  30562  erclwwlktr  30643  erclwwlkntr  30692  eucrctshift  30874  frgr3v  30906  frgr2wwlkeqm  30962  xrofsup  33429  lmhmimasvsca  33669  erdszelem8  36130  cvmliftmolem2  36214  cvmlift2lem12  36246  r1peuqusdeg1  36575  btwnswapid  36960  btwnsegle  37060  broutsideof3  37069  outsidele  37075  nmulprop  37117  nmulcom  37121  isbasisrelowllem2  38471  cvrletrN  40522  ltltncvr  40672  atcvrj2b  40681  cvrat4  40692  2at0mat0  40774  islpln2a  40797  paddasslem11  41079  pmod1i  41097  lautcvr  41341  cdlemg4c  41861  tendoplass  42032  tendodi1  42033  tendodi2  42034  mendlmod  44383  mendassa  44384  3adantlr3  46262  ssinc  46307  ssdec  46308  ioondisj2  46710  ioondisj1  46711  stoweidlem60  47275  ply1mulgsumlem2  49704  lincresunit3lem2  49797  catprs  50330  fthcomf  50478  oppcthinco  50779  oppcthinendcALT  50781