Theorem simplr3 1219

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soltmin  6099  frfi  9195  wemappo  9464  ttrclss  9641  ttrclselem2  9647  iccsplit  13438  ccatswrd  14631  pfxccat3  14696  modfsummods  15756  pcdvdstr  16847  vdwlem12  16963  cshwsidrepswmod0  17065  iscatd2  17647  oppccomfpropd  17693  initoeu2lem0  17980  resssetc  18059  resscatc  18076  yonedalem4c  18243  mod1ile  18459  mod2ile  18460  prdssgrpd  18701  prdsmndd  18738  grprcan  18949  mulgnn0dir  19080  mulgdir  19082  mulgass  19087  mulgnn0di  19800  mulgdi  19801  dprd2da  20019  submomnd  20107  ogrpaddltbi  20114  lmodprop2d  20919  lssintcl  20959  prdslmodd  20964  islmhm2  21033  islbs2  21152  islbs3  21153  dmatmul  22462  mdetmul  22588  restopnb  23140  iunconn  23393  1stcelcls  23426  blsscls2  24469  stdbdbl  24482  xrsblre  24777  icccmplem2  24789  itg1val2  25651  cvxcl  26948  conway  27771  leadds1  27981  addsass  27997  mulscom  28131  addonbday  28271  colline  28717  tglowdim2ln  28719  f1otrg  28939  f1otrge  28940  ax5seglem4  29001  ax5seglem5  29002  axcontlem3  29035  axcontlem8  29040  axcontlem9  29041  eengtrkg  29055  frgr3v  30345  xrofsup  32840  lmhmimasvsca  33099  erdszelem8  35380  resconn  35428  cvmliftmolem2  35464  cvmlift2lem12  35496  r1peuqusdeg1  35825  broutsideof3  36308  outsideoftr  36311  outsidele  36314  ltltncvr  39869  atcvrj2b  39878  cvrat4  39889  cvrat42  39890  2at0mat0  39971  islpln2a  39994  paddasslem11  40276  pmod1i  40294  lhpm0atN  40475  lautcvr  40538  cdlemg4c  41058  tendoplass  41229  tendodi1  41230  tendodi2  41231  dgrsub2  43563  grumnud  44713  ssinc  45517  ssdec  45518  ioondisj2  45923  ioondisj1  45924  ply1mulgsumlem2  48863  catprs  49486  fthcomf  49632  oppcthinco  49914  oppcthinendcALT  49916