Theorem simp1r 1007

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 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1003	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simpl1r  1034  simpr1r  1040  simp11r  1094  simp21r  1100  simp31r  1106  vtoclgft  2762  en2lp  4511  funprg  5217  nnsucsssuc  6432  ecopovtrn  6570  ecopovtrng  6573  addassnqg  7285  distrnqg  7290  ltsonq  7301  ltanqg  7303  ltmnqg  7304  distrnq0  7362  addassnq0  7365  prarloclem5  7403  recexprlem1ssl  7536  recexprlem1ssu  7537  mulasssrg  7661  distrsrg  7662  lttrsr  7665  ltsosr  7667  ltasrg  7673  mulextsr1lem  7683  mulextsr1  7684  axmulass  7776  axdistr  7777  dmdcanap  8578  lt2msq1  8739  lediv2  8745  xaddass2  9756  xlt2add  9766  modqdi  10273  expaddzaplem  10444  expaddzap  10445  expmulzap  10447  bdtrilem  11120  xrbdtri  11155  prmexpb  12005  cnptoprest  12599  ssblps  12785  ssbl  12786  rplogbchbase  13227  rplogbreexp  13230  relogbcxpbap  13242