Theorem simplr3 1227

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  soltmin  6113  frfi  9218  wemappo  9487  ttrclss  9665  ttrclselem2  9671  iccsplit  13479  ccatswrd  14672  pfxccat3  14737  modfsummods  15797  pcdvdstr  16888  vdwlem12  17004  cshwsidrepswmod0  17106  iscatd2  17689  oppccomfpropd  17735  initoeu2lem0  18022  resssetc  18101  resscatc  18118  yonedalem4c  18285  mod1ile  18501  mod2ile  18502  prdssgrpd  18743  prdsmndd  18780  grprcan  18991  mulgnn0dir  19122  mulgdir  19124  mulgass  19129  mulgnn0di  19841  mulgdi  19842  dprd2da  20060  submomnd  20148  ogrpaddltbi  20155  lmodprop2d  20964  lssintcl  21004  prdslmodd  21009  islmhm2  21078  islbs2  21197  islbs3  21198  dmatmul  22530  mdetmul  22656  restopnb  23208  iunconn  23461  1stcelcls  23494  blsscls2  24537  stdbdbl  24550  xrsblre  24845  icccmplem2  24857  itg1val2  25719  cvxcl  27019  conway  27842  leadds1  28052  addsass  28068  mulscom  28202  addonbday  28342  colline  28788  tglowdim2ln  28790  f1otrg  29010  f1otrge  29011  ax5seglem4  29072  ax5seglem5  29073  axcontlem3  29106  axcontlem8  29111  axcontlem9  29112  eengtrkg  29126  frgr3v  30416  xrofsup  32912  lmhmimasvsca  33171  erdszelem8  35496  resconn  35544  cvmliftmolem2  35580  cvmlift2lem12  35612  r1peuqusdeg1  35941  broutsideof3  36424  outsideoftr  36427  outsidele  36430  nmulprop  36488  nmulcom  36492  ltltncvr  39995  atcvrj2b  40004  cvrat4  40015  cvrat42  40016  2at0mat0  40097  islpln2a  40120  paddasslem11  40402  pmod1i  40420  lhpm0atN  40601  lautcvr  40664  cdlemg4c  41184  tendoplass  41355  tendodi1  41356  tendodi2  41357  dgrsub2  43660  grumnud  44810  ssinc  45613  ssdec  45614  ioondisj2  46017  ioondisj1  46018  ply1mulgsumlem2  48957  catprs  49580  fthcomf  49726  oppcthinco  50008  oppcthinendcALT  50010