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  4703  funprg  5434  nnsucsssuc  6770  ecopovtrn  6911  ecopovtrng  6914  addassnqg  7756  distrnqg  7761  ltsonq  7772  ltanqg  7774  ltmnqg  7775  distrnq0  7833  addassnq0  7836  prarloclem5  7874  recexprlem1ssl  8007  recexprlem1ssu  8008  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  dmdcanap  9061  lt2msq1  9224  lediv2  9230  xaddass2  10289  xlt2add  10299  modqdi  10850  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  swrdspsleq  11461  pfxeq  11490  bdtrilem  12030  xrbdtri  12067  bitsfzo  12747  prmexpb  12955  4sqlem18  13216  mgmsscl  13740  subgabl  14226  rng1zrlem  14365  cnptoprest  15498  ssblps  15684  ssbl  15685  rplogbchbase  16219  rplogbreexp  16222  relogbcxpbap  16234  lgssq  16397  uhgr2edg  16685