Theorem simplr3 1098

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simplr3	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simpr3 1062	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	adantr 480	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  soltmin  5451  frfi  8090  wemappo  8337  iccsplit  12176  ccatswrd  13308  swrdccat3  13343  pcdvdstr  15418  vdwlem12  15534  cshwsidrepswmod0  15639  iscatd2  16165  oppccomfpropd  16210  initoeu2lem0  16486  resssetc  16565  resscatc  16578  yonedalem4c  16740  mod1ile  16928  mod2ile  16929  prdsmndd  17146  grprcan  17278  mulgnn0dir  17394  mulgdir  17396  mulgass  17402  mulgnn0di  18054  mulgdi  18055  dprd2da  18264  lmodprop2d  18748  lssintcl  18785  prdslmodd  18790  islmhm2  18859  islbs2  18975  islbs3  18976  dmatmul  20122  mdetmul  20248  restopnb  20789  iuncon  21041  1stcelcls  21074  blsscls2  22119  stdbdbl  22132  xrsblre  22422  icccmplem2  22434  itg1val2  23257  cvxcl  24511  colline  25344  tglowdim2ln  25346  f1otrg  25551  f1otrge  25552  ax5seglem4  25612  ax5seglem5  25613  axcontlem3  25646  axcontlem8  25651  axcontlem9  25652  eengtrkg  25665  el2wlksotot  26409  xrofsup  28923  submomnd  29041  ogrpaddltbi  29050  erdszelem8  30434  rescon  30482  cvmliftmolem2  30518  cvmlift2lem12  30550  broutsideof3  31403  outsideoftr  31406  outsidele  31409  ltltncvr  33727  atcvrj2b  33736  cvrat4  33747  cvrat42  33748  2at0mat0  33829  islpln2a  33852  paddasslem11  34134  pmod1i  34152  lhpm0atN  34333  lautcvr  34396  cdlemg4c  34918  tendoplass  35089  tendodi1  35090  tendodi2  35091  dgrsub2  36724  ssinc  38292  ssdec  38293  ioondisj2  38561  ioondisj1  38562  pfxccat3  40289  frgr3v  41445  ply1mulgsumlem2  41969