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  2810  en2lp  4586  funprg  5304  nnsucsssuc  6545  ecopovtrn  6686  ecopovtrng  6689  addassnqg  7442  distrnqg  7447  ltsonq  7458  ltanqg  7460  ltmnqg  7461  distrnq0  7519  addassnq0  7522  prarloclem5  7560  recexprlem1ssl  7693  recexprlem1ssu  7694  mulasssrg  7818  distrsrg  7819  lttrsr  7822  ltsosr  7824  ltasrg  7830  mulextsr1lem  7840  mulextsr1  7841  axmulass  7933  axdistr  7934  dmdcanap  8741  lt2msq1  8904  lediv2  8910  xaddass2  9936  xlt2add  9946  modqdi  10463  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  bdtrilem  11382  xrbdtri  11419  prmexpb  12289  4sqlem18  12546  mgmsscl  12944  subgabl  13402  cnptoprest  14407  ssblps  14593  ssbl  14594  rplogbchbase  15082  rplogbreexp  15085  relogbcxpbap  15097  lgssq  15156