Theorem simplr3 1218

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 726	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  soltmin  6138  frfi  9288  wemappo  9544  ttrclss  9715  ttrclselem2  9721  iccsplit  13462  ccatswrd  14618  pfxccat3  14684  modfsummods  15739  pcdvdstr  16809  vdwlem12  16925  cshwsidrepswmod0  17028  iscatd2  17625  oppccomfpropd  17673  initoeu2lem0  17963  resssetc  18042  resscatc  18059  yonedalem4c  18230  mod1ile  18446  mod2ile  18447  prdssgrpd  18624  prdsmndd  18658  grprcan  18858  mulgnn0dir  18984  mulgdir  18986  mulgass  18991  mulgnn0di  19693  mulgdi  19694  dprd2da  19912  lmodprop2d  20534  lssintcl  20575  prdslmodd  20580  islmhm2  20649  islbs2  20767  islbs3  20768  dmatmul  21999  mdetmul  22125  restopnb  22679  iunconn  22932  1stcelcls  22965  blsscls2  24013  stdbdbl  24026  xrsblre  24327  icccmplem2  24339  itg1val2  25201  cvxcl  26489  conway  27300  sleadd1  27472  addsass  27488  mulscom  27595  colline  27900  tglowdim2ln  27902  f1otrg  28122  f1otrge  28123  ax5seglem4  28190  ax5seglem5  28191  axcontlem3  28224  axcontlem8  28229  axcontlem9  28230  eengtrkg  28244  frgr3v  29528  xrofsup  31980  submomnd  32228  ogrpaddltbi  32236  erdszelem8  34189  resconn  34237  cvmliftmolem2  34273  cvmlift2lem12  34305  broutsideof3  35098  outsideoftr  35101  outsidele  35104  ltltncvr  38294  atcvrj2b  38303  cvrat4  38314  cvrat42  38315  2at0mat0  38396  islpln2a  38419  paddasslem11  38701  pmod1i  38719  lhpm0atN  38900  lautcvr  38963  cdlemg4c  39483  tendoplass  39654  tendodi1  39655  tendodi2  39656  dgrsub2  41877  grumnud  43045  ssinc  43776  ssdec  43777  ioondisj2  44206  ioondisj1  44207  ply1mulgsumlem2  47068  catprs  47631