Theorem simplr3 1105

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

Assertion

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

Proof of Theorem simplr3

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soltmin  5532  frfi  8205  wemappo  8454  iccsplit  12305  ccatswrd  13456  swrdccat3  13492  modfsummods  14525  pcdvdstr  15580  vdwlem12  15696  cshwsidrepswmod0  15801  iscatd2  16342  oppccomfpropd  16387  initoeu2lem0  16663  resssetc  16742  resscatc  16755  yonedalem4c  16917  mod1ile  17105  mod2ile  17106  prdsmndd  17323  grprcan  17455  mulgnn0dir  17571  mulgdir  17573  mulgass  17579  mulgnn0di  18231  mulgdi  18232  dprd2da  18441  lmodprop2d  18925  lssintcl  18964  prdslmodd  18969  islmhm2  19038  islbs2  19154  islbs3  19155  dmatmul  20303  mdetmul  20429  restopnb  20979  iunconn  21231  1stcelcls  21264  blsscls2  22309  stdbdbl  22322  xrsblre  22614  icccmplem2  22626  itg1val2  23451  cvxcl  24711  colline  25544  tglowdim2ln  25546  f1otrg  25751  f1otrge  25752  ax5seglem4  25812  ax5seglem5  25813  axcontlem3  25846  axcontlem8  25851  axcontlem9  25852  eengtrkg  25865  frgr3v  27139  xrofsup  29533  submomnd  29710  ogrpaddltbi  29719  erdszelem8  31180  resconn  31228  cvmliftmolem2  31264  cvmlift2lem12  31296  conway  31910  broutsideof3  32233  outsideoftr  32236  outsidele  32239  ltltncvr  34709  atcvrj2b  34718  cvrat4  34729  cvrat42  34730  2at0mat0  34811  islpln2a  34834  paddasslem11  35116  pmod1i  35134  lhpm0atN  35315  lautcvr  35378  cdlemg4c  35900  tendoplass  36071  tendodi1  36072  tendodi2  36073  dgrsub2  37705  ssinc  39264  ssdec  39265  ioondisj2  39714  ioondisj1  39715  pfxccat3  41426  ply1mulgsumlem2  42175