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  4439  funprg  5405  fsnunf  5883  f1oiso2  5999  tfrlemibxssdm  6557  ecopovtrn  6865  ecopovtrng  6868  dftap2  7564  addassnqg  7696  ltsonq  7712  ltanqg  7714  ltmnqg  7715  addassnq0  7776  recexprlem1ssl  7947  mulasssrg  8072  distrsrg  8073  lttrsr  8076  ltsosr  8078  ltasrg  8084  mulextsr1lem  8094  mulextsr1  8095  axmulass  8187  axdistr  8188  dmdcanap  8995  lediv2  9164  ltdiv23  9165  lediv23  9166  xaddass2  10202  xlt2add  10212  expaddzaplem  10943  expaddzap  10944  expmulzap  10946  expdivap  10951  leisorel  11205  swrdspsleq  11355  pfxeq  11384  ccatopth2  11405  bdtrilem  11920  xrbdtri  11957  fldivndvdslt  12619  prmexpb  12844  pcpremul  12987  pcdiv  12996  pcqmul  12997  pcqdiv  13001  4sqlem12  13096  f1ocpbllem  13515  ercpbl  13536  erlecpbl  13537  cmn4  14014  ablsub4  14022  abladdsub4  14023  cnptoprest  15096  ssblps  15282  ssbl  15283  tgqioo  15412  plyadd  15608  plymul  15609  rplogbchbase  15807