Theorem simp2r 966

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  simpl2r  993  simpr2r  999  simp12r  1053  simp22r  1059  simp32r  1065  issod  4082  funprg  4980  fsnunf  5394  f1oiso2  5497  tfrlemibxssdm  5976  ecopovtrn  6269  ecopovtrng  6272  addassnqg  6634  ltsonq  6650  ltanqg  6652  ltmnqg  6653  addassnq0  6714  recexprlem1ssl  6885  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  mulextsr1lem  7018  mulextsr1  7019  axmulass  7101  axdistr  7102  dmdcanap  7877  lediv2  8036  ltdiv23  8037  lediv23  8038  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  expdivap  9624  fldivndvdslt  10479  prmexpb  10674