Theorem simp2r 1020

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 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1015	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 974

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

This theorem depends on definitions:  df-bi 116  df-3an 976

This theorem is referenced by:  simpl2r  1047  simpr2r  1053  simp12r  1107  simp22r  1113  simp32r  1119  issod  4305  funprg  5250  fsnunf  5700  f1oiso2  5810  tfrlemibxssdm  6310  ecopovtrn  6614  ecopovtrng  6617  addassnqg  7348  ltsonq  7364  ltanqg  7366  ltmnqg  7367  addassnq0  7428  recexprlem1ssl  7599  mulasssrg  7724  distrsrg  7725  lttrsr  7728  ltsosr  7730  ltasrg  7736  mulextsr1lem  7746  mulextsr1  7747  axmulass  7839  axdistr  7840  dmdcanap  8643  lediv2  8811  ltdiv23  8812  lediv23  8813  xaddass2  9831  xlt2add  9841  expaddzaplem  10523  expaddzap  10524  expmulzap  10526  expdivap  10531  leisorel  10776  bdtrilem  11206  xrbdtri  11243  fldivndvdslt  11898  prmexpb  12109  pcpremul  12251  pcdiv  12260  pcqmul  12261  pcqdiv  12265  cnptoprest  13118  ssblps  13304  ssbl  13305  tgqioo  13426  rplogbchbase  13747