Theorem simplr3 1219

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  soltmin  5981  frfi  8894  wemappo  9143  iccsplit  13038  ccatswrd  14198  pfxccat3  14264  modfsummods  15320  pcdvdstr  16392  vdwlem12  16508  cshwsidrepswmod0  16611  iscatd2  17138  oppccomfpropd  17185  initoeu2lem0  17473  resssetc  17552  resscatc  17569  yonedalem4c  17739  mod1ile  17953  mod2ile  17954  prdsmndd  18160  grprcan  18355  mulgnn0dir  18475  mulgdir  18477  mulgass  18482  mulgnn0di  19165  mulgdi  19166  dprd2da  19383  lmodprop2d  19915  lssintcl  19955  prdslmodd  19960  islmhm2  20029  islbs2  20145  islbs3  20146  dmatmul  21348  mdetmul  21474  restopnb  22026  iunconn  22279  1stcelcls  22312  blsscls2  23356  stdbdbl  23369  xrsblre  23662  icccmplem2  23674  itg1val2  24535  cvxcl  25821  colline  26694  tglowdim2ln  26696  f1otrg  26916  f1otrge  26917  ax5seglem4  26977  ax5seglem5  26978  axcontlem3  27011  axcontlem8  27016  axcontlem9  27017  eengtrkg  27031  frgr3v  28312  xrofsup  30764  submomnd  31009  ogrpaddltbi  31017  erdszelem8  32827  resconn  32875  cvmliftmolem2  32911  cvmlift2lem12  32943  conway  33679  broutsideof3  34114  outsideoftr  34117  outsidele  34120  ltltncvr  37123  atcvrj2b  37132  cvrat4  37143  cvrat42  37144  2at0mat0  37225  islpln2a  37248  paddasslem11  37530  pmod1i  37548  lhpm0atN  37729  lautcvr  37792  cdlemg4c  38312  tendoplass  38483  tendodi1  38484  tendodi2  38485  dgrsub2  40604  grumnud  41518  ssinc  42251  ssdec  42252  ioondisj2  42647  ioondisj1  42648  ply1mulgsumlem2  45344  catprs  45908