Theorem simplr3 1216

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  soltmin  6034  frfi  9046  wemappo  9295  ttrclss  9465  ttrclselem2  9471  iccsplit  13227  ccatswrd  14391  pfxccat3  14457  modfsummods  15515  pcdvdstr  16587  vdwlem12  16703  cshwsidrepswmod0  16806  iscatd2  17400  oppccomfpropd  17448  initoeu2lem0  17738  resssetc  17817  resscatc  17834  yonedalem4c  18005  mod1ile  18221  mod2ile  18222  prdsmndd  18428  grprcan  18623  mulgnn0dir  18743  mulgdir  18745  mulgass  18750  mulgnn0di  19437  mulgdi  19438  dprd2da  19655  lmodprop2d  20195  lssintcl  20236  prdslmodd  20241  islmhm2  20310  islbs2  20426  islbs3  20427  dmatmul  21656  mdetmul  21782  restopnb  22336  iunconn  22589  1stcelcls  22622  blsscls2  23670  stdbdbl  23683  xrsblre  23984  icccmplem2  23996  itg1val2  24858  cvxcl  26144  colline  27020  tglowdim2ln  27022  f1otrg  27242  f1otrge  27243  ax5seglem4  27310  ax5seglem5  27311  axcontlem3  27344  axcontlem8  27349  axcontlem9  27350  eengtrkg  27364  frgr3v  28647  xrofsup  31098  submomnd  31344  ogrpaddltbi  31352  erdszelem8  33168  resconn  33216  cvmliftmolem2  33252  cvmlift2lem12  33284  conway  34001  broutsideof3  34436  outsideoftr  34439  outsidele  34442  ltltncvr  37445  atcvrj2b  37454  cvrat4  37465  cvrat42  37466  2at0mat0  37547  islpln2a  37570  paddasslem11  37852  pmod1i  37870  lhpm0atN  38051  lautcvr  38114  cdlemg4c  38634  tendoplass  38805  tendodi1  38806  tendodi2  38807  dgrsub2  40968  grumnud  41885  ssinc  42618  ssdec  42619  ioondisj2  43012  ioondisj1  43013  ply1mulgsumlem2  45706  catprs  46270