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  6083  frfi  9169  wemappo  9435  ttrclss  9610  ttrclselem2  9616  iccsplit  13382  ccatswrd  14573  pfxccat3  14638  modfsummods  15697  pcdvdstr  16785  vdwlem12  16901  cshwsidrepswmod0  17003  iscatd2  17584  oppccomfpropd  17630  initoeu2lem0  17917  resssetc  17996  resscatc  18013  yonedalem4c  18180  mod1ile  18396  mod2ile  18397  prdssgrpd  18638  prdsmndd  18675  grprcan  18883  mulgnn0dir  19014  mulgdir  19016  mulgass  19021  mulgnn0di  19735  mulgdi  19736  dprd2da  19954  submomnd  20042  ogrpaddltbi  20049  lmodprop2d  20855  lssintcl  20895  prdslmodd  20900  islmhm2  20970  islbs2  21089  islbs3  21090  dmatmul  22410  mdetmul  22536  restopnb  23088  iunconn  23341  1stcelcls  23374  blsscls2  24417  stdbdbl  24430  xrsblre  24725  icccmplem2  24737  itg1val2  25610  cvxcl  26920  conway  27738  sleadd1  27930  addsass  27946  mulscom  28076  colline  28625  tglowdim2ln  28627  f1otrg  28847  f1otrge  28848  ax5seglem4  28908  ax5seglem5  28909  axcontlem3  28942  axcontlem8  28947  axcontlem9  28948  eengtrkg  28962  frgr3v  30250  xrofsup  32745  lmhmimasvsca  33015  erdszelem8  35230  resconn  35278  cvmliftmolem2  35314  cvmlift2lem12  35346  r1peuqusdeg1  35675  broutsideof3  36159  outsideoftr  36162  outsidele  36165  ltltncvr  39461  atcvrj2b  39470  cvrat4  39481  cvrat42  39482  2at0mat0  39563  islpln2a  39586  paddasslem11  39868  pmod1i  39886  lhpm0atN  40067  lautcvr  40130  cdlemg4c  40650  tendoplass  40821  tendodi1  40822  tendodi2  40823  dgrsub2  43167  grumnud  44318  ssinc  45123  ssdec  45124  ioondisj2  45532  ioondisj1  45533  ply1mulgsumlem2  48418  catprs  49042  fthcomf  49188  oppcthinco  49470  oppcthinendcALT  49472