Theorem simp1r 1049

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

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

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 1007

This theorem is referenced by:  simpl1r  1076  simpr1r  1082  simp11r  1136  simp21r  1142  simp31r  1148  vtoclgft  2864  en2lp  4675  funprg  5405  nnsucsssuc  6724  ecopovtrn  6865  ecopovtrng  6868  addassnqg  7696  distrnqg  7701  ltsonq  7712  ltanqg  7714  ltmnqg  7715  distrnq0  7773  addassnq0  7776  prarloclem5  7814  recexprlem1ssl  7947  recexprlem1ssu  7948  mulasssrg  8072  distrsrg  8073  lttrsr  8076  ltsosr  8078  ltasrg  8084  mulextsr1lem  8094  mulextsr1  8095  axmulass  8187  axdistr  8188  dmdcanap  8995  lt2msq1  9158  lediv2  9164  xaddass2  10202  xlt2add  10212  modqdi  10753  expaddzaplem  10943  expaddzap  10944  expmulzap  10946  swrdspsleq  11355  pfxeq  11384  bdtrilem  11920  xrbdtri  11957  bitsfzo  12637  prmexpb  12844  4sqlem18  13102  mgmsscl  13566  subgabl  14041  cnptoprest  15096  ssblps  15282  ssbl  15283  rplogbchbase  15807  rplogbreexp  15810  relogbcxpbap  15822  lgssq  15905  uhgr2edg  16193