Theorem simp2r 1048

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

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

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 1004

This theorem is referenced by:  simpl2r  1075  simpr2r  1081  simp12r  1135  simp22r  1141  simp32r  1147  issod  4410  funprg  5371  fsnunf  5839  f1oiso2  5951  tfrlemibxssdm  6473  ecopovtrn  6779  ecopovtrng  6782  dftap2  7437  addassnqg  7569  ltsonq  7585  ltanqg  7587  ltmnqg  7588  addassnq0  7649  recexprlem1ssl  7820  mulasssrg  7945  distrsrg  7946  lttrsr  7949  ltsosr  7951  ltasrg  7957  mulextsr1lem  7967  mulextsr1  7968  axmulass  8060  axdistr  8061  dmdcanap  8869  lediv2  9038  ltdiv23  9039  lediv23  9040  xaddass2  10066  xlt2add  10076  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  expdivap  10812  leisorel  11059  swrdspsleq  11199  pfxeq  11228  ccatopth2  11249  bdtrilem  11750  xrbdtri  11787  fldivndvdslt  12448  prmexpb  12673  pcpremul  12816  pcdiv  12825  pcqmul  12826  pcqdiv  12830  4sqlem12  12925  f1ocpbllem  13343  ercpbl  13364  erlecpbl  13365  cmn4  13842  ablsub4  13850  abladdsub4  13851  cnptoprest  14913  ssblps  15099  ssbl  15100  tgqioo  15229  plyadd  15425  plymul  15426  rplogbchbase  15624