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 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  6155  frfi  9322  wemappo  9590  ttrclss  9761  ttrclselem2  9767  iccsplit  13526  ccatswrd  14707  pfxccat3  14773  modfsummods  15830  pcdvdstr  16915  vdwlem12  17031  cshwsidrepswmod0  17133  iscatd2  17725  oppccomfpropd  17771  initoeu2lem0  18059  resssetc  18138  resscatc  18155  yonedalem4c  18323  mod1ile  18539  mod2ile  18540  prdssgrpd  18747  prdsmndd  18784  grprcan  18992  mulgnn0dir  19123  mulgdir  19125  mulgass  19130  mulgnn0di  19844  mulgdi  19845  dprd2da  20063  lmodprop2d  20923  lssintcl  20963  prdslmodd  20968  islmhm2  21038  islbs2  21157  islbs3  21158  dmatmul  22504  mdetmul  22630  restopnb  23184  iunconn  23437  1stcelcls  23470  blsscls2  24518  stdbdbl  24531  xrsblre  24834  icccmplem2  24846  itg1val2  25720  cvxcl  27029  conway  27845  sleadd1  28023  addsass  28039  mulscom  28166  colline  28658  tglowdim2ln  28660  f1otrg  28880  f1otrge  28881  ax5seglem4  28948  ax5seglem5  28949  axcontlem3  28982  axcontlem8  28987  axcontlem9  28988  eengtrkg  29002  frgr3v  30295  xrofsup  32772  lmhmimasvsca  33045  submomnd  33088  ogrpaddltbi  33096  erdszelem8  35204  resconn  35252  cvmliftmolem2  35288  cvmlift2lem12  35320  r1peuqusdeg1  35649  broutsideof3  36128  outsideoftr  36131  outsidele  36134  ltltncvr  39426  atcvrj2b  39435  cvrat4  39446  cvrat42  39447  2at0mat0  39528  islpln2a  39551  paddasslem11  39833  pmod1i  39851  lhpm0atN  40032  lautcvr  40095  cdlemg4c  40615  tendoplass  40786  tendodi1  40787  tendodi2  40788  dgrsub2  43152  grumnud  44310  ssinc  45097  ssdec  45098  ioondisj2  45511  ioondisj1  45512  ply1mulgsumlem2  48309  catprs  48915  oppcthinco  49113  oppcthinendcALT  49115