Theorem simplr3 1218

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 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  6109  frfi  9232  wemappo  9502  ttrclss  9673  ttrclselem2  9679  iccsplit  13446  ccatswrd  14633  pfxccat3  14699  modfsummods  15759  pcdvdstr  16847  vdwlem12  16963  cshwsidrepswmod0  17065  iscatd2  17642  oppccomfpropd  17688  initoeu2lem0  17975  resssetc  18054  resscatc  18071  yonedalem4c  18238  mod1ile  18452  mod2ile  18453  prdssgrpd  18660  prdsmndd  18697  grprcan  18905  mulgnn0dir  19036  mulgdir  19038  mulgass  19043  mulgnn0di  19755  mulgdi  19756  dprd2da  19974  lmodprop2d  20830  lssintcl  20870  prdslmodd  20875  islmhm2  20945  islbs2  21064  islbs3  21065  dmatmul  22384  mdetmul  22510  restopnb  23062  iunconn  23315  1stcelcls  23348  blsscls2  24392  stdbdbl  24405  xrsblre  24700  icccmplem2  24712  itg1val2  25585  cvxcl  26895  conway  27711  sleadd1  27896  addsass  27912  mulscom  28042  colline  28576  tglowdim2ln  28578  f1otrg  28798  f1otrge  28799  ax5seglem4  28859  ax5seglem5  28860  axcontlem3  28893  axcontlem8  28898  axcontlem9  28899  eengtrkg  28913  frgr3v  30204  xrofsup  32690  lmhmimasvsca  32980  submomnd  33024  ogrpaddltbi  33032  erdszelem8  35185  resconn  35233  cvmliftmolem2  35269  cvmlift2lem12  35301  r1peuqusdeg1  35630  broutsideof3  36114  outsideoftr  36117  outsidele  36120  ltltncvr  39417  atcvrj2b  39426  cvrat4  39437  cvrat42  39438  2at0mat0  39519  islpln2a  39542  paddasslem11  39824  pmod1i  39842  lhpm0atN  40023  lautcvr  40086  cdlemg4c  40606  tendoplass  40777  tendodi1  40778  tendodi2  40779  dgrsub2  43124  grumnud  44275  ssinc  45081  ssdec  45082  ioondisj2  45491  ioondisj1  45492  ply1mulgsumlem2  48376  catprs  49000  fthcomf  49146  oppcthinco  49428  oppcthinendcALT  49430