Theorem simp1r 1049

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 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1045	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:  simpl1r  1076  simpr1r  1082  simp11r  1136  simp21r  1142  simp31r  1148  vtoclgft  2867  en2lp  4681  funprg  5411  nnsucsssuc  6738  ecopovtrn  6879  ecopovtrng  6882  addassnqg  7713  distrnqg  7718  ltsonq  7729  ltanqg  7731  ltmnqg  7732  distrnq0  7790  addassnq0  7793  prarloclem5  7831  recexprlem1ssl  7964  recexprlem1ssu  7965  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  dmdcanap  9013  lt2msq1  9176  lediv2  9182  xaddass2  10222  xlt2add  10232  modqdi  10778  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  swrdspsleq  11384  pfxeq  11413  bdtrilem  11949  xrbdtri  11986  bitsfzo  12666  prmexpb  12873  4sqlem18  13131  mgmsscl  13658  subgabl  14133  cnptoprest  15216  ssblps  15402  ssbl  15403  rplogbchbase  15927  rplogbreexp  15930  relogbcxpbap  15942  lgssq  16025  uhgr2edg  16313