Theorem simp2r 1051

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

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

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 1007

This theorem is referenced by:  simpl2r  1078  simpr2r  1084  simp12r  1138  simp22r  1144  simp32r  1150  issod  4422  funprg  5387  fsnunf  5862  f1oiso2  5978  tfrlemibxssdm  6536  ecopovtrn  6844  ecopovtrng  6847  dftap2  7513  addassnqg  7645  ltsonq  7661  ltanqg  7663  ltmnqg  7664  addassnq0  7725  recexprlem1ssl  7896  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  dmdcanap  8945  lediv2  9114  ltdiv23  9115  lediv23  9116  xaddass2  10148  xlt2add  10158  expaddzaplem  10888  expaddzap  10889  expmulzap  10891  expdivap  10896  leisorel  11145  swrdspsleq  11295  pfxeq  11324  ccatopth2  11345  bdtrilem  11860  xrbdtri  11897  fldivndvdslt  12559  prmexpb  12784  pcpremul  12927  pcdiv  12936  pcqmul  12937  pcqdiv  12941  4sqlem12  13036  f1ocpbllem  13454  ercpbl  13475  erlecpbl  13476  cmn4  13953  ablsub4  13961  abladdsub4  13962  cnptoprest  15030  ssblps  15216  ssbl  15217  tgqioo  15346  plyadd  15542  plymul  15543  rplogbchbase  15741