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  4445  funprg  5411  fsnunf  5889  f1oiso2  6006  tfrlemibxssdm  6571  ecopovtrn  6879  ecopovtrng  6882  dftap2  7581  addassnqg  7713  ltsonq  7729  ltanqg  7731  ltmnqg  7732  addassnq0  7793  recexprlem1ssl  7964  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  dmdcanap  9013  lediv2  9182  ltdiv23  9183  lediv23  9184  xaddass2  10222  xlt2add  10232  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  expdivap  10976  leisorel  11234  swrdspsleq  11384  pfxeq  11413  ccatopth2  11434  bdtrilem  11949  xrbdtri  11986  fldivndvdslt  12648  prmexpb  12873  pcpremul  13016  pcdiv  13025  pcqmul  13026  pcqdiv  13030  4sqlem12  13125  f1ocpbllem  13607  ercpbl  13628  erlecpbl  13629  cmn4  14106  ablsub4  14114  abladdsub4  14115  cnptoprest  15216  ssblps  15402  ssbl  15403  tgqioo  15532  plyadd  15728  plymul  15729  rplogbchbase  15927