Theorem simplr3 1216

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soltmin  6159  frfi  9319  wemappo  9587  ttrclss  9758  ttrclselem2  9764  iccsplit  13522  ccatswrd  14703  pfxccat3  14769  modfsummods  15826  pcdvdstr  16910  vdwlem12  17026  cshwsidrepswmod0  17129  iscatd2  17726  oppccomfpropd  17774  initoeu2lem0  18067  resssetc  18146  resscatc  18163  yonedalem4c  18334  mod1ile  18551  mod2ile  18552  prdssgrpd  18759  prdsmndd  18796  grprcan  19004  mulgnn0dir  19135  mulgdir  19137  mulgass  19142  mulgnn0di  19858  mulgdi  19859  dprd2da  20077  lmodprop2d  20939  lssintcl  20980  prdslmodd  20985  islmhm2  21055  islbs2  21174  islbs3  21175  dmatmul  22519  mdetmul  22645  restopnb  23199  iunconn  23452  1stcelcls  23485  blsscls2  24533  stdbdbl  24546  xrsblre  24847  icccmplem2  24859  itg1val2  25733  cvxcl  27043  conway  27859  sleadd1  28037  addsass  28053  mulscom  28180  colline  28672  tglowdim2ln  28674  f1otrg  28894  f1otrge  28895  ax5seglem4  28962  ax5seglem5  28963  axcontlem3  28996  axcontlem8  29001  axcontlem9  29002  eengtrkg  29016  frgr3v  30304  xrofsup  32778  lmhmimasvsca  33027  submomnd  33070  ogrpaddltbi  33078  erdszelem8  35183  resconn  35231  cvmliftmolem2  35267  cvmlift2lem12  35299  r1peuqusdeg1  35628  broutsideof3  36108  outsideoftr  36111  outsidele  36114  ltltncvr  39406  atcvrj2b  39415  cvrat4  39426  cvrat42  39427  2at0mat0  39508  islpln2a  39531  paddasslem11  39813  pmod1i  39831  lhpm0atN  40012  lautcvr  40075  cdlemg4c  40595  tendoplass  40766  tendodi1  40767  tendodi2  40768  dgrsub2  43124  grumnud  44282  ssinc  45027  ssdec  45028  ioondisj2  45446  ioondisj1  45447  ply1mulgsumlem2  48233  catprs  48800