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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soltmin  6101  frfi  9197  wemappo  9466  ttrclss  9641  ttrclselem2  9647  iccsplit  13413  ccatswrd  14604  pfxccat3  14669  modfsummods  15728  pcdvdstr  16816  vdwlem12  16932  cshwsidrepswmod0  17034  iscatd2  17616  oppccomfpropd  17662  initoeu2lem0  17949  resssetc  18028  resscatc  18045  yonedalem4c  18212  mod1ile  18428  mod2ile  18429  prdssgrpd  18670  prdsmndd  18707  grprcan  18915  mulgnn0dir  19046  mulgdir  19048  mulgass  19053  mulgnn0di  19766  mulgdi  19767  dprd2da  19985  submomnd  20073  ogrpaddltbi  20080  lmodprop2d  20887  lssintcl  20927  prdslmodd  20932  islmhm2  21002  islbs2  21121  islbs3  21122  dmatmul  22453  mdetmul  22579  restopnb  23131  iunconn  23384  1stcelcls  23417  blsscls2  24460  stdbdbl  24473  xrsblre  24768  icccmplem2  24780  itg1val2  25653  cvxcl  26963  conway  27787  leadds1  27997  addsass  28013  mulscom  28147  addonbday  28287  colline  28733  tglowdim2ln  28735  f1otrg  28955  f1otrge  28956  ax5seglem4  29017  ax5seglem5  29018  axcontlem3  29051  axcontlem8  29056  axcontlem9  29057  eengtrkg  29071  frgr3v  30362  xrofsup  32857  lmhmimasvsca  33131  erdszelem8  35411  resconn  35459  cvmliftmolem2  35495  cvmlift2lem12  35527  r1peuqusdeg1  35856  broutsideof3  36339  outsideoftr  36342  outsidele  36345  ltltncvr  39793  atcvrj2b  39802  cvrat4  39813  cvrat42  39814  2at0mat0  39895  islpln2a  39918  paddasslem11  40200  pmod1i  40218  lhpm0atN  40399  lautcvr  40462  cdlemg4c  40982  tendoplass  41153  tendodi1  41154  tendodi2  41155  dgrsub2  43486  grumnud  44636  ssinc  45440  ssdec  45441  ioondisj2  45847  ioondisj1  45848  ply1mulgsumlem2  48741  catprs  49364  fthcomf  49510  oppcthinco  49792  oppcthinendcALT  49794