Theorem simp1r 1022

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 1018	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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 980

This theorem is referenced by:  simpl1r  1049  simpr1r  1055  simp11r  1109  simp21r  1115  simp31r  1121  vtoclgft  2789  en2lp  4555  funprg  5268  nnsucsssuc  6495  ecopovtrn  6634  ecopovtrng  6637  addassnqg  7383  distrnqg  7388  ltsonq  7399  ltanqg  7401  ltmnqg  7402  distrnq0  7460  addassnq0  7463  prarloclem5  7501  recexprlem1ssl  7634  recexprlem1ssu  7635  mulasssrg  7759  distrsrg  7760  lttrsr  7763  ltsosr  7765  ltasrg  7771  mulextsr1lem  7781  mulextsr1  7782  axmulass  7874  axdistr  7875  dmdcanap  8681  lt2msq1  8844  lediv2  8850  xaddass2  9872  xlt2add  9882  modqdi  10394  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  bdtrilem  11249  xrbdtri  11286  prmexpb  12153  mgmsscl  12785  cnptoprest  13778  ssblps  13964  ssbl  13965  rplogbchbase  14407  rplogbreexp  14410  relogbcxpbap  14422  lgssq  14480