Theorem simp2r 1024

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

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

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 980

This theorem is referenced by:  simpl2r  1051  simpr2r  1057  simp12r  1111  simp22r  1117  simp32r  1123  issod  4313  funprg  5258  fsnunf  5708  f1oiso2  5818  tfrlemibxssdm  6318  ecopovtrn  6622  ecopovtrng  6625  addassnqg  7356  ltsonq  7372  ltanqg  7374  ltmnqg  7375  addassnq0  7436  recexprlem1ssl  7607  mulasssrg  7732  distrsrg  7733  lttrsr  7736  ltsosr  7738  ltasrg  7744  mulextsr1lem  7754  mulextsr1  7755  axmulass  7847  axdistr  7848  dmdcanap  8651  lediv2  8819  ltdiv23  8820  lediv23  8821  xaddass2  9839  xlt2add  9849  expaddzaplem  10531  expaddzap  10532  expmulzap  10534  expdivap  10539  leisorel  10783  bdtrilem  11213  xrbdtri  11250  fldivndvdslt  11905  prmexpb  12116  pcpremul  12258  pcdiv  12267  pcqmul  12268  pcqdiv  12272  cmn4  12904  ablsub4  12912  abladdsub4  12913  cnptoprest  13290  ssblps  13476  ssbl  13477  tgqioo  13598  rplogbchbase  13919