Theorem simplr3 1236

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6141  frfi  9255  wemappo  9521  ttrclss  9699  ttrclselem2  9705  iccsplit  13530  ccatswrd  14730  pfxccat3  14795  modfsummods  15871  pcdvdstr  16961  vdwlem12  17077  cshwsidrepswmod0  17179  iscatd2  17762  oppccomfpropd  17808  initoeu2lem0  18095  resssetc  18174  resscatc  18191  yonedalem4c  18358  mod1ile  18574  mod2ile  18575  prdssgrpd  18820  prdsmndd  18859  grprcan  19071  mulgnn0dir  19201  mulgdir  19203  mulgass  19208  mulgnn0di  19926  mulgdi  19927  dprd2da  20145  submomnd  20233  ogrpaddltbi  20240  lmodprop2d  21082  lssintcl  21122  prdslmodd  21127  islmhm2  21196  islbs2  21315  islbs3  21316  dmatmul  22691  mdetmul  22817  restopnb  23369  iunconn  23622  1stcelcls  23655  blsscls2  24698  stdbdbl  24711  xrsblre  25006  icccmplem2  25018  itg1val2  25880  cvxcl  27186  conway  28009  leadds1  28219  addsass  28235  mulscom  28369  addonbday  28509  colline  28960  tglowdim2ln  28962  f1otrg  29257  f1otrge  29258  ax5seglem4  29319  ax5seglem5  29320  axcontlem3  29353  axcontlem8  29358  axcontlem9  29359  eengtrkg  29373  frgr3v  30663  xrofsup  33149  lmhmimasvsca  33389  erdszelem8  35711  resconn  35759  cvmliftmolem2  35795  cvmlift2lem12  35827  r1peuqusdeg1  36156  broutsideof3  36639  outsideoftr  36642  outsidele  36645  nmulprop  36703  nmulcom  36707  ltltncvr  40238  atcvrj2b  40247  cvrat4  40258  cvrat42  40259  2at0mat0  40340  islpln2a  40363  paddasslem11  40645  pmod1i  40663  lhpm0atN  40844  lautcvr  40907  cdlemg4c  41427  tendoplass  41598  tendodi1  41599  tendodi2  41600  dgrsub2  43903  grumnud  45037  ssinc  45846  ssdec  45847  ioondisj2  46250  ioondisj1  46251  ply1mulgsumlem2  49208  catprs  49830  fthcomf  49976  oppcthinco  50258  oppcthinendcALT  50260