Theorem simp1r 1006

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1r	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1002	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl1r  1033  simpr1r  1039  simp11r  1093  simp21r  1099  simp31r  1105  vtoclgft  2736  en2lp  4469  funprg  5173  nnsucsssuc  6388  ecopovtrn  6526  ecopovtrng  6529  addassnqg  7190  distrnqg  7195  ltsonq  7206  ltanqg  7208  ltmnqg  7209  distrnq0  7267  addassnq0  7270  prarloclem5  7308  recexprlem1ssl  7441  recexprlem1ssu  7442  mulasssrg  7566  distrsrg  7567  lttrsr  7570  ltsosr  7572  ltasrg  7578  mulextsr1lem  7588  mulextsr1  7589  axmulass  7681  axdistr  7682  dmdcanap  8482  lt2msq1  8643  lediv2  8649  xaddass2  9653  xlt2add  9663  modqdi  10165  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  bdtrilem  11010  xrbdtri  11045  prmexpb  11829  cnptoprest  12408  ssblps  12594  ssbl  12595