Theorem simp2r 1026

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1021	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl2r  1053  simpr2r  1059  simp12r  1113  simp22r  1119  simp32r  1125  issod  4355  funprg  5309  fsnunf  5765  f1oiso2  5877  tfrlemibxssdm  6394  ecopovtrn  6700  ecopovtrng  6703  dftap2  7336  addassnqg  7468  ltsonq  7484  ltanqg  7486  ltmnqg  7487  addassnq0  7548  recexprlem1ssl  7719  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  dmdcanap  8768  lediv2  8937  ltdiv23  8938  lediv23  8939  xaddass2  9964  xlt2add  9974  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  expdivap  10701  leisorel  10948  bdtrilem  11423  xrbdtri  11460  fldivndvdslt  12121  prmexpb  12346  pcpremul  12489  pcdiv  12498  pcqmul  12499  pcqdiv  12503  4sqlem12  12598  f1ocpbllem  13014  ercpbl  13035  erlecpbl  13036  cmn4  13513  ablsub4  13521  abladdsub4  13522  cnptoprest  14583  ssblps  14769  ssbl  14770  tgqioo  14899  plyadd  15095  plymul  15096  rplogbchbase  15294