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  4646  funprg  5371  nnsucsssuc  6646  ecopovtrn  6787  ecopovtrng  6790  addassnqg  7577  distrnqg  7582  ltsonq  7593  ltanqg  7595  ltmnqg  7596  distrnq0  7654  addassnq0  7657  prarloclem5  7695  recexprlem1ssl  7828  recexprlem1ssu  7829  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  dmdcanap  8877  lt2msq1  9040  lediv2  9046  xaddass2  10074  xlt2add  10084  modqdi  10622  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  swrdspsleq  11207  pfxeq  11236  bdtrilem  11758  xrbdtri  11795  bitsfzo  12474  prmexpb  12681  4sqlem18  12939  mgmsscl  13402  subgabl  13877  cnptoprest  14921  ssblps  15107  ssbl  15108  rplogbchbase  15632  rplogbreexp  15635  relogbcxpbap  15647  lgssq  15727  uhgr2edg  16012