Theorem simp2r 1055

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2r  1082  simpr2r  1088  simp12r  1142  simp22r  1148  simp32r  1154  issod  4464  funprg  5431  fsnunf  5915  f1oiso2  6033  tfrlemibxssdm  6598  ecopovtrn  6906  ecopovtrng  6909  dftap2  7618  addassnqg  7750  ltsonq  7766  ltanqg  7768  ltmnqg  7769  addassnq0  7830  recexprlem1ssl  8001  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  dmdcanap  9055  lediv2  9224  ltdiv23  9225  lediv23  9226  xaddass2  10283  xlt2add  10293  expaddzaplem  11033  expaddzap  11034  expmulzap  11036  expdivap  11041  leisorel  11304  swrdspsleq  11454  pfxeq  11483  ccatopth2  11504  bdtrilem  12023  xrbdtri  12060  fldivndvdslt  12722  prmexpb  12948  pcpremul  13094  pcdiv  13103  pcqmul  13104  pcqdiv  13108  4sqlem12  13203  f1ocpbllem  13682  ercpbl  13703  erlecpbl  13704  cmn4  14159  ablsub4  14168  abladdsub4  14169  cnptoprest  15392  ssblps  15578  ssbl  15579  tgqioo  15708  plyadd  15904  plymul  15905  rplogbchbase  16108  dichmul0or  16882