Theorem simp1r 1053

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1r  1080  simpr1r  1086  simp11r  1140  simp21r  1146  simp31r  1152  vtoclgft  2873  en2lp  4701  funprg  5431  nnsucsssuc  6765  ecopovtrn  6906  ecopovtrng  6909  addassnqg  7750  distrnqg  7755  ltsonq  7766  ltanqg  7768  ltmnqg  7769  distrnq0  7827  addassnq0  7830  prarloclem5  7868  recexprlem1ssl  8001  recexprlem1ssu  8002  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  dmdcanap  9055  lt2msq1  9218  lediv2  9224  xaddass2  10283  xlt2add  10293  modqdi  10843  expaddzaplem  11033  expaddzap  11034  expmulzap  11036  swrdspsleq  11454  pfxeq  11483  bdtrilem  12023  xrbdtri  12060  bitsfzo  12740  prmexpb  12948  4sqlem18  13209  mgmsscl  13732  subgabl  14187  rng1zrlem  14309  cnptoprest  15392  ssblps  15578  ssbl  15579  rplogbchbase  16108  rplogbreexp  16111  relogbcxpbap  16123  lgssq  16281  uhgr2edg  16569