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  5843  f1oiso2  5957  tfrlemibxssdm  6479  ecopovtrn  6787  ecopovtrng  6790  dftap2  7445  addassnqg  7577  ltsonq  7593  ltanqg  7595  ltmnqg  7596  addassnq0  7657  recexprlem1ssl  7828  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  dmdcanap  8877  lediv2  9046  ltdiv23  9047  lediv23  9048  xaddass2  10074  xlt2add  10084  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  expdivap  10820  leisorel  11067  swrdspsleq  11207  pfxeq  11236  ccatopth2  11257  bdtrilem  11758  xrbdtri  11795  fldivndvdslt  12456  prmexpb  12681  pcpremul  12824  pcdiv  12833  pcqmul  12834  pcqdiv  12838  4sqlem12  12933  f1ocpbllem  13351  ercpbl  13372  erlecpbl  13373  cmn4  13850  ablsub4  13858  abladdsub4  13859  cnptoprest  14921  ssblps  15107  ssbl  15108  tgqioo  15237  plyadd  15433  plymul  15434  rplogbchbase  15632