Theorem simp1r 1024

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

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

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 982

This theorem is referenced by:  simpl1r  1051  simpr1r  1057  simp11r  1111  simp21r  1117  simp31r  1123  vtoclgft  2814  en2lp  4590  funprg  5308  nnsucsssuc  6550  ecopovtrn  6691  ecopovtrng  6694  addassnqg  7449  distrnqg  7454  ltsonq  7465  ltanqg  7467  ltmnqg  7468  distrnq0  7526  addassnq0  7529  prarloclem5  7567  recexprlem1ssl  7700  recexprlem1ssu  7701  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1lem  7847  mulextsr1  7848  axmulass  7940  axdistr  7941  dmdcanap  8749  lt2msq1  8912  lediv2  8918  xaddass2  9945  xlt2add  9955  modqdi  10484  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  bdtrilem  11404  xrbdtri  11441  bitsfzo  12119  prmexpb  12319  4sqlem18  12577  mgmsscl  13004  subgabl  13462  cnptoprest  14475  ssblps  14661  ssbl  14662  rplogbchbase  15186  rplogbreexp  15189  relogbcxpbap  15201  lgssq  15281