Theorem simplr3 1236

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6134  frfi  9259  wemappo  9525  ttrclss  9703  ttrclselem2  9709  iccsplit  13542  ccatswrd  14742  pfxccat3  14807  modfsummods  15884  pcdvdstr  16974  vdwlem12  17090  cshwsidrepswmod0  17192  iscatd2  17775  oppccomfpropd  17821  initoeu2lem0  18108  resssetc  18187  resscatc  18204  yonedalem4c  18371  mod1ile  18587  mod2ile  18588  prdssgrpd  18841  prdsmndd  18883  grprcan  19103  mulgnn0dir  19233  mulgdir  19235  mulgass  19240  mulgnn0di  19958  mulgdi  19959  dprd2da  20177  submomnd  20265  ogrpaddltbi  20272  lmodprop2d  21114  lssintcl  21154  prdslmodd  21159  islmhm2  21228  islbs2  21347  islbs3  21348  dmatmul  22725  mdetmul  22851  restopnb  23406  iunconn  23659  1stcelcls  23693  blsscls2  24736  stdbdbl  24749  xrsblre  25044  icccmplem2  25056  itg1val2  25918  cvxcl  27229  conway  28052  leadds1  28262  addsass  28278  mulscom  28412  addonbday  28552  colline  29005  tglowdim2ln  29007  f1otrg  29335  f1otrge  29336  ax5seglem4  29397  ax5seglem5  29398  axcontlem3  29431  axcontlem8  29436  axcontlem9  29437  eengtrkg  29451  frgr3v  30763  xrofsup  33246  lmhmimasvsca  33486  erdszelem8  35785  resconn  35833  cvmliftmolem2  35869  cvmlift2lem12  35901  r1peuqusdeg1  36230  broutsideof3  36714  outsideoftr  36717  outsidele  36720  nmulprop  36778  nmulcom  36782  ltltncvr  40304  atcvrj2b  40313  cvrat4  40324  cvrat42  40325  2at0mat0  40406  islpln2a  40429  paddasslem11  40711  pmod1i  40729  lhpm0atN  40910  lautcvr  40973  cdlemg4c  41493  tendoplass  41664  tendodi1  41665  tendodi2  41666  dgrsub2  43984  grumnud  45118  ssinc  45927  ssdec  45928  ioondisj2  46331  ioondisj1  46332  ply1mulgsumlem2  49325  catprs  49945  fthcomf  50091  oppcthinco  50373  oppcthinendcALT  50375