Theorem simp1r 1046

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 1042	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:  simpl1r  1073  simpr1r  1079  simp11r  1133  simp21r  1139  simp31r  1145  vtoclgft  2852  en2lp  4650  funprg  5377  nnsucsssuc  6655  ecopovtrn  6796  ecopovtrng  6799  addassnqg  7595  distrnqg  7600  ltsonq  7611  ltanqg  7613  ltmnqg  7614  distrnq0  7672  addassnq0  7675  prarloclem5  7713  recexprlem1ssl  7846  recexprlem1ssu  7847  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  dmdcanap  8895  lt2msq1  9058  lediv2  9064  xaddass2  10098  xlt2add  10108  modqdi  10647  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  swrdspsleq  11241  pfxeq  11270  bdtrilem  11793  xrbdtri  11830  bitsfzo  12509  prmexpb  12716  4sqlem18  12974  mgmsscl  13437  subgabl  13912  cnptoprest  14956  ssblps  15142  ssbl  15143  rplogbchbase  15667  rplogbreexp  15670  relogbcxpbap  15682  lgssq  15762  uhgr2edg  16050