Theorem simplr3 1215

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  soltmin  6038  frfi  9020  wemappo  9269  ttrclss  9439  ttrclselem2  9445  iccsplit  13199  ccatswrd  14362  pfxccat3  14428  modfsummods  15486  pcdvdstr  16558  vdwlem12  16674  cshwsidrepswmod0  16777  iscatd2  17371  oppccomfpropd  17419  initoeu2lem0  17709  resssetc  17788  resscatc  17805  yonedalem4c  17976  mod1ile  18192  mod2ile  18193  prdsmndd  18399  grprcan  18594  mulgnn0dir  18714  mulgdir  18716  mulgass  18721  mulgnn0di  19408  mulgdi  19409  dprd2da  19626  lmodprop2d  20166  lssintcl  20207  prdslmodd  20212  islmhm2  20281  islbs2  20397  islbs3  20398  dmatmul  21627  mdetmul  21753  restopnb  22307  iunconn  22560  1stcelcls  22593  blsscls2  23641  stdbdbl  23654  xrsblre  23955  icccmplem2  23967  itg1val2  24829  cvxcl  26115  colline  26991  tglowdim2ln  26993  f1otrg  27213  f1otrge  27214  ax5seglem4  27281  ax5seglem5  27282  axcontlem3  27315  axcontlem8  27320  axcontlem9  27321  eengtrkg  27335  frgr3v  28618  xrofsup  31069  submomnd  31315  ogrpaddltbi  31323  erdszelem8  33139  resconn  33187  cvmliftmolem2  33223  cvmlift2lem12  33255  conway  33972  broutsideof3  34407  outsideoftr  34410  outsidele  34413  ltltncvr  37416  atcvrj2b  37425  cvrat4  37436  cvrat42  37437  2at0mat0  37518  islpln2a  37541  paddasslem11  37823  pmod1i  37841  lhpm0atN  38022  lautcvr  38085  cdlemg4c  38605  tendoplass  38776  tendodi1  38777  tendodi2  38778  dgrsub2  40940  grumnud  41857  ssinc  42590  ssdec  42591  ioondisj2  42985  ioondisj1  42986  ply1mulgsumlem2  45680  catprs  46244