Theorem simplr3 1217

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 725	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  soltmin  6134  frfi  9284  wemappo  9540  ttrclss  9711  ttrclselem2  9717  iccsplit  13458  ccatswrd  14614  pfxccat3  14680  modfsummods  15735  pcdvdstr  16805  vdwlem12  16921  cshwsidrepswmod0  17024  iscatd2  17621  oppccomfpropd  17669  initoeu2lem0  17959  resssetc  18038  resscatc  18055  yonedalem4c  18226  mod1ile  18442  mod2ile  18443  prdssgrpd  18620  prdsmndd  18654  grprcan  18854  mulgnn0dir  18978  mulgdir  18980  mulgass  18985  mulgnn0di  19687  mulgdi  19688  dprd2da  19906  lmodprop2d  20526  lssintcl  20567  prdslmodd  20572  islmhm2  20641  islbs2  20759  islbs3  20760  dmatmul  21990  mdetmul  22116  restopnb  22670  iunconn  22923  1stcelcls  22956  blsscls2  24004  stdbdbl  24017  xrsblre  24318  icccmplem2  24330  itg1val2  25192  cvxcl  26478  conway  27289  sleadd1  27461  addsass  27477  mulscom  27584  colline  27889  tglowdim2ln  27891  f1otrg  28111  f1otrge  28112  ax5seglem4  28179  ax5seglem5  28180  axcontlem3  28213  axcontlem8  28218  axcontlem9  28219  eengtrkg  28233  frgr3v  29517  xrofsup  31967  submomnd  32215  ogrpaddltbi  32223  erdszelem8  34177  resconn  34225  cvmliftmolem2  34261  cvmlift2lem12  34293  broutsideof3  35086  outsideoftr  35089  outsidele  35092  ltltncvr  38282  atcvrj2b  38291  cvrat4  38302  cvrat42  38303  2at0mat0  38384  islpln2a  38407  paddasslem11  38689  pmod1i  38707  lhpm0atN  38888  lautcvr  38951  cdlemg4c  39471  tendoplass  39642  tendodi1  39643  tendodi2  39644  dgrsub2  41862  grumnud  43030  ssinc  43761  ssdec  43762  ioondisj2  44192  ioondisj1  44193  ply1mulgsumlem2  47021  catprs  47584