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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soltmin  6087  frfi  9176  wemappo  9442  ttrclss  9617  ttrclselem2  9623  iccsplit  13387  ccatswrd  14578  pfxccat3  14643  modfsummods  15702  pcdvdstr  16790  vdwlem12  16906  cshwsidrepswmod0  17008  iscatd2  17589  oppccomfpropd  17635  initoeu2lem0  17922  resssetc  18001  resscatc  18018  yonedalem4c  18185  mod1ile  18401  mod2ile  18402  prdssgrpd  18643  prdsmndd  18680  grprcan  18888  mulgnn0dir  19019  mulgdir  19021  mulgass  19026  mulgnn0di  19739  mulgdi  19740  dprd2da  19958  submomnd  20046  ogrpaddltbi  20053  lmodprop2d  20859  lssintcl  20899  prdslmodd  20904  islmhm2  20974  islbs2  21093  islbs3  21094  dmatmul  22413  mdetmul  22539  restopnb  23091  iunconn  23344  1stcelcls  23377  blsscls2  24420  stdbdbl  24433  xrsblre  24728  icccmplem2  24740  itg1val2  25613  cvxcl  26923  conway  27741  sleadd1  27933  addsass  27949  mulscom  28079  colline  28628  tglowdim2ln  28630  f1otrg  28850  f1otrge  28851  ax5seglem4  28912  ax5seglem5  28913  axcontlem3  28946  axcontlem8  28951  axcontlem9  28952  eengtrkg  28966  frgr3v  30257  xrofsup  32754  lmhmimasvsca  33027  erdszelem8  35263  resconn  35311  cvmliftmolem2  35347  cvmlift2lem12  35379  r1peuqusdeg1  35708  broutsideof3  36191  outsideoftr  36194  outsidele  36197  ltltncvr  39542  atcvrj2b  39551  cvrat4  39562  cvrat42  39563  2at0mat0  39644  islpln2a  39667  paddasslem11  39949  pmod1i  39967  lhpm0atN  40148  lautcvr  40211  cdlemg4c  40731  tendoplass  40902  tendodi1  40903  tendodi2  40904  dgrsub2  43252  grumnud  44403  ssinc  45208  ssdec  45209  ioondisj2  45617  ioondisj1  45618  ply1mulgsumlem2  48512  catprs  49136  fthcomf  49282  oppcthinco  49564  oppcthinendcALT  49566