Theorem simplr3 1217

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 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 726	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  6168  frfi  9349  wemappo  9618  ttrclss  9789  ttrclselem2  9795  iccsplit  13545  ccatswrd  14716  pfxccat3  14782  modfsummods  15841  pcdvdstr  16923  vdwlem12  17039  cshwsidrepswmod0  17142  iscatd2  17739  oppccomfpropd  17787  initoeu2lem0  18080  resssetc  18159  resscatc  18176  yonedalem4c  18347  mod1ile  18563  mod2ile  18564  prdssgrpd  18771  prdsmndd  18805  grprcan  19013  mulgnn0dir  19144  mulgdir  19146  mulgass  19151  mulgnn0di  19867  mulgdi  19868  dprd2da  20086  lmodprop2d  20944  lssintcl  20985  prdslmodd  20990  islmhm2  21060  islbs2  21179  islbs3  21180  dmatmul  22524  mdetmul  22650  restopnb  23204  iunconn  23457  1stcelcls  23490  blsscls2  24538  stdbdbl  24551  xrsblre  24852  icccmplem2  24864  itg1val2  25738  cvxcl  27046  conway  27862  sleadd1  28040  addsass  28056  mulscom  28183  colline  28675  tglowdim2ln  28677  f1otrg  28897  f1otrge  28898  ax5seglem4  28965  ax5seglem5  28966  axcontlem3  28999  axcontlem8  29004  axcontlem9  29005  eengtrkg  29019  frgr3v  30307  xrofsup  32774  lmhmimasvsca  33025  submomnd  33060  ogrpaddltbi  33068  erdszelem8  35166  resconn  35214  cvmliftmolem2  35250  cvmlift2lem12  35282  r1peuqusdeg1  35611  broutsideof3  36090  outsideoftr  36093  outsidele  36096  ltltncvr  39380  atcvrj2b  39389  cvrat4  39400  cvrat42  39401  2at0mat0  39482  islpln2a  39505  paddasslem11  39787  pmod1i  39805  lhpm0atN  39986  lautcvr  40049  cdlemg4c  40569  tendoplass  40740  tendodi1  40741  tendodi2  40742  dgrsub2  43092  grumnud  44255  ssinc  44989  ssdec  44990  ioondisj2  45411  ioondisj1  45412  ply1mulgsumlem2  48116  catprs  48678