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  2851  en2lp  4643  funprg  5367  nnsucsssuc  6628  ecopovtrn  6769  ecopovtrng  6772  addassnqg  7557  distrnqg  7562  ltsonq  7573  ltanqg  7575  ltmnqg  7576  distrnq0  7634  addassnq0  7637  prarloclem5  7675  recexprlem1ssl  7808  recexprlem1ssu  7809  mulasssrg  7933  distrsrg  7934  lttrsr  7937  ltsosr  7939  ltasrg  7945  mulextsr1lem  7955  mulextsr1  7956  axmulass  8048  axdistr  8049  dmdcanap  8857  lt2msq1  9020  lediv2  9026  xaddass2  10054  xlt2add  10064  modqdi  10601  expaddzaplem  10791  expaddzap  10792  expmulzap  10794  swrdspsleq  11185  pfxeq  11214  bdtrilem  11736  xrbdtri  11773  bitsfzo  12452  prmexpb  12659  4sqlem18  12917  mgmsscl  13380  subgabl  13855  cnptoprest  14898  ssblps  15084  ssbl  15085  rplogbchbase  15609  rplogbreexp  15612  relogbcxpbap  15624  lgssq  15704  uhgr2edg  15989