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  6129  frfi  9279  wemappo  9546  ttrclss  9724  ttrclselem2  9730  iccsplit  13619  ccatswrd  14822  pfxccat3  14887  modfsummods  15965  pcdvdstr  17059  vdwlem12  17175  cshwsidrepswmod0  17277  iscatd2  17860  oppccomfpropd  17906  initoeu2lem0  18193  resssetc  18272  resscatc  18289  yonedalem4c  18456  mod1ile  18672  mod2ile  18673  prdssgrpd  18927  prdsmndd  18969  grprcan  19189  mulgnn0dir  19319  mulgdir  19321  mulgass  19326  mulgnn0di  20044  mulgdi  20045  dprd2da  20263  submomnd  20351  ogrpaddltbi  20358  lmodprop2d  21204  lssintcl  21244  prdslmodd  21249  islmhm2  21318  islbs2  21437  islbs3  21438  dmatmul  22817  mdetmul  22943  restopnb  23498  iunconn  23751  1stcelcls  23785  blsscls2  24828  stdbdbl  24841  xrsblre  25136  icccmplem2  25148  itg1val2  26010  cvxcl  27317  conway  28170  leadds1  28380  addsass  28396  mulscom  28530  addonbday  28670  colline  29123  tglowdim2ln  29125  f1otrg  29453  f1otrge  29454  ax5seglem4  29515  ax5seglem5  29516  axcontlem3  29549  axcontlem8  29554  axcontlem9  29555  eengtrkg  29569  frgr3v  30881  xrofsup  33405  lmhmimasvsca  33645  erdszelem8  36049  resconn  36097  cvmliftmolem2  36133  cvmlift2lem12  36165  r1peuqusdeg1  36494  broutsideof3  36983  outsideoftr  36986  outsidele  36989  nmulprop  37031  nmulcom  37035  ltltncvr  40573  atcvrj2b  40582  cvrat4  40593  cvrat42  40594  2at0mat0  40675  islpln2a  40698  paddasslem11  40980  pmod1i  40998  lhpm0atN  41179  lautcvr  41242  cdlemg4c  41762  tendoplass  41933  tendodi1  41934  tendodi2  41935  dgrsub2  44230  grumnud  45363  ssinc  46195  ssdec  46196  ioondisj2  46598  ioondisj1  46599  ply1mulgsumlem2  49592  catprs  50218  fthcomf  50366  oppcthinco  50667  oppcthinendcALT  50669