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 725	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  soltmin  6056  frfi  9103  wemappo  9352  ttrclss  9522  ttrclselem2  9528  iccsplit  13263  ccatswrd  14426  pfxccat3  14492  modfsummods  15550  pcdvdstr  16622  vdwlem12  16738  cshwsidrepswmod0  16841  iscatd2  17435  oppccomfpropd  17483  initoeu2lem0  17773  resssetc  17852  resscatc  17869  yonedalem4c  18040  mod1ile  18256  mod2ile  18257  prdsmndd  18463  grprcan  18658  mulgnn0dir  18778  mulgdir  18780  mulgass  18785  mulgnn0di  19472  mulgdi  19473  dprd2da  19690  lmodprop2d  20230  lssintcl  20271  prdslmodd  20276  islmhm2  20345  islbs2  20461  islbs3  20462  dmatmul  21691  mdetmul  21817  restopnb  22371  iunconn  22624  1stcelcls  22657  blsscls2  23705  stdbdbl  23718  xrsblre  24019  icccmplem2  24031  itg1val2  24893  cvxcl  26179  colline  27055  tglowdim2ln  27057  f1otrg  27277  f1otrge  27278  ax5seglem4  27345  ax5seglem5  27346  axcontlem3  27379  axcontlem8  27384  axcontlem9  27385  eengtrkg  27399  frgr3v  28684  xrofsup  31135  submomnd  31381  ogrpaddltbi  31389  erdszelem8  33205  resconn  33253  cvmliftmolem2  33289  cvmlift2lem12  33321  conway  34038  broutsideof3  34473  outsideoftr  34476  outsidele  34479  ltltncvr  37479  atcvrj2b  37488  cvrat4  37499  cvrat42  37500  2at0mat0  37581  islpln2a  37604  paddasslem11  37886  pmod1i  37904  lhpm0atN  38085  lautcvr  38148  cdlemg4c  38668  tendoplass  38839  tendodi1  38840  tendodi2  38841  dgrsub2  40998  grumnud  41942  ssinc  42675  ssdec  42676  ioondisj2  43080  ioondisj1  43081  ply1mulgsumlem2  45786  catprs  46350