Theorem simp2r 1048

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

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

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 1004

This theorem is referenced by:  simpl2r  1075  simpr2r  1081  simp12r  1135  simp22r  1141  simp32r  1147  issod  4414  funprg  5377  fsnunf  5849  f1oiso2  5963  tfrlemibxssdm  6488  ecopovtrn  6796  ecopovtrng  6799  dftap2  7463  addassnqg  7595  ltsonq  7611  ltanqg  7613  ltmnqg  7614  addassnq0  7675  recexprlem1ssl  7846  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  dmdcanap  8895  lediv2  9064  ltdiv23  9065  lediv23  9066  xaddass2  10098  xlt2add  10108  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  expdivap  10845  leisorel  11094  swrdspsleq  11241  pfxeq  11270  ccatopth2  11291  bdtrilem  11793  xrbdtri  11830  fldivndvdslt  12491  prmexpb  12716  pcpremul  12859  pcdiv  12868  pcqmul  12869  pcqdiv  12873  4sqlem12  12968  f1ocpbllem  13386  ercpbl  13407  erlecpbl  13408  cmn4  13885  ablsub4  13893  abladdsub4  13894  cnptoprest  14956  ssblps  15142  ssbl  15143  tgqioo  15272  plyadd  15468  plymul  15469  rplogbchbase  15667