Theorem simplr3 1236

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr3	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simp3 1156	. 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  ttrclss  9748  ttrclselem2  9754  iccsplit  13643  ccatswrd  14846  pfxccat3  14911  modfsummods  15989  pcdvdstr  17083  vdwlem12  17199  cshwsidrepswmod0  17301  iscatd2  17884  oppccomfpropd  17930  initoeu2lem0  18217  resssetc  18296  resscatc  18313  yonedalem4c  18480  mod1ile  18696  mod2ile  18697  prdssgrpd  18951  prdsmndd  18993  grprcan  19213  mulgnn0dir  19343  mulgdir  19345  mulgass  19350  mulgnn0di  20069  mulgdi  20070  dprd2da  20288  submomnd  20376  ogrpaddltbi  20383  lmodprop2d  21229  lssintcl  21269  prdslmodd  21274  islmhm2  21343  islbs2  21462  islbs3  21463  dmatmul  22842  mdetmul  22968  restopnb  23523  iunconn  23776  1stcelcls  23810  blsscls2  24853  stdbdbl  24866  xrsblre  25161  icccmplem2  25173  itg1val2  26035  cvxcl  27342  conway  28195  leadds1  28405  addsass  28421  mulscom  28555  addonbday  28695  colline  29148  tglowdim2ln  29150  f1otrg  29478  f1otrge  29479  ax5seglem4  29540  ax5seglem5  29541  axcontlem3  29574  axcontlem8  29579  axcontlem9  29580  eengtrkg  29594  frgr3v  30906  xrofsup  33429  lmhmimasvsca  33669  erdszelem8  36130  resconn  36178  cvmliftmolem2  36214  cvmlift2lem12  36246  r1peuqusdeg1  36575  broutsideof3  37069  outsideoftr  37072  outsidele  37075  nmulprop  37117  nmulcom  37121  ltltncvr  40672  atcvrj2b  40681  cvrat4  40692  cvrat42  40693  2at0mat0  40774  islpln2a  40797  paddasslem11  41079  pmod1i  41097  lhpm0atN  41278  lautcvr  41341  cdlemg4c  41861  tendoplass  42032  tendodi1  42033  tendodi2  42034  dgrsub2  44329  grumnud  45462  ssinc  46307  ssdec  46308  ioondisj2  46710  ioondisj1  46711  ply1mulgsumlem2  49704  catprs  50330  fthcomf  50478  oppcthinco  50779  oppcthinendcALT  50781