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  6128  frfi  9260  wemappo  9527  ttrclss  9705  ttrclselem2  9711  iccsplit  13597  ccatswrd  14798  pfxccat3  14863  modfsummods  15940  pcdvdstr  17034  vdwlem12  17150  cshwsidrepswmod0  17252  iscatd2  17835  oppccomfpropd  17881  initoeu2lem0  18168  resssetc  18247  resscatc  18264  yonedalem4c  18431  mod1ile  18647  mod2ile  18648  prdssgrpd  18902  prdsmndd  18944  grprcan  19164  mulgnn0dir  19294  mulgdir  19296  mulgass  19301  mulgnn0di  20019  mulgdi  20020  dprd2da  20238  submomnd  20326  ogrpaddltbi  20333  lmodprop2d  21179  lssintcl  21219  prdslmodd  21224  islmhm2  21293  islbs2  21412  islbs3  21413  dmatmul  22792  mdetmul  22918  restopnb  23473  iunconn  23726  1stcelcls  23760  blsscls2  24803  stdbdbl  24816  xrsblre  25111  icccmplem2  25123  itg1val2  25985  cvxcl  27294  conway  28147  leadds1  28357  addsass  28373  mulscom  28507  addonbday  28647  colline  29100  tglowdim2ln  29102  f1otrg  29430  f1otrge  29431  ax5seglem4  29492  ax5seglem5  29493  axcontlem3  29526  axcontlem8  29531  axcontlem9  29532  eengtrkg  29546  frgr3v  30858  xrofsup  33341  lmhmimasvsca  33581  erdszelem8  35932  resconn  35980  cvmliftmolem2  36016  cvmlift2lem12  36048  r1peuqusdeg1  36377  broutsideof3  36861  outsideoftr  36864  outsidele  36867  nmulprop  36909  nmulcom  36913  ltltncvr  40448  atcvrj2b  40457  cvrat4  40468  cvrat42  40469  2at0mat0  40550  islpln2a  40573  paddasslem11  40855  pmod1i  40873  lhpm0atN  41054  lautcvr  41117  cdlemg4c  41637  tendoplass  41808  tendodi1  41809  tendodi2  41810  dgrsub2  44095  grumnud  45229  ssinc  46045  ssdec  46046  ioondisj2  46449  ioondisj1  46450  ply1mulgsumlem2  49443  catprs  50063  fthcomf  50209  oppcthinco  50491  oppcthinendcALT  50493