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  6141  frfi  9255  wemappo  9521  iccsplit  13530  ccatswrd  14730  pcdvdstr  16961  vdwlem12  17077  iscatd2  17762  oppccomfpropd  17808  resssetc  18174  resscatc  18191  mod1ile  18574  mod2ile  18575  prdssgrpd  18820  prdsmndd  18859  grprcan  19071  mulgnn0dir  19201  mulgnn0di  19926  mulgdi  19927  submomnd  20233  ogrpaddltbi  20240  lmodprop2d  21082  lssintcl  21122  prdslmodd  21127  islmhm2  21196  islbs3  21316  mdetmul  22817  restopnb  23369  nrmsep  23551  iunconn  23622  ptpjopn  23806  blsscls2  24698  xrsblre  25006  icccmplem2  25018  icccvx  25146  conway  28009  addsass  28235  mulscom  28369  addonbday  28509  colline  28960  tglowdim2ln  28962  f1otrg  29257  f1otrge  29258  ax5seglem5  29320  axcontlem3  29353  axcontlem4  29354  axcontlem8  29358  eengtrkg  29373  2pthon3v  30329  erclwwlktr  30410  erclwwlkntr  30459  eucrctshift  30631  frgr3v  30663  frgr2wwlkeqm  30719  xrofsup  33149  lmhmimasvsca  33389  erdszelem8  35711  cvmliftmolem2  35795  cvmlift2lem12  35827  r1peuqusdeg1  36156  btwnswapid  36530  btwnsegle  36630  broutsideof3  36639  outsidele  36645  nmulprop  36703  nmulcom  36707  isbasisrelowllem2  38043  cvrletrN  40088  ltltncvr  40238  atcvrj2b  40247  cvrat4  40258  2at0mat0  40340  islpln2a  40363  paddasslem11  40645  pmod1i  40663  lautcvr  40907  cdlemg4c  41427  tendoplass  41598  tendodi1  41599  tendodi2  41600  mendlmod  43957  mendassa  43958  3adantlr3  45801  ssinc  45846  ssdec  45847  ioondisj2  46250  ioondisj1  46251  stoweidlem60  46815  ply1mulgsumlem2  49208  lincresunit3lem2  49301  catprs  49830  fthcomf  49976  oppcthinco  50258  oppcthinendcALT  50260