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

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

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 1011

This theorem is referenced by:  simpl1r  1080  simpr1r  1086  simp11r  1140  simp21r  1146  simp31r  1152  vtoclgft  2873  en2lp  4699  funprg  5429  nnsucsssuc  6759  ecopovtrn  6900  ecopovtrng  6903  addassnqg  7743  distrnqg  7748  ltsonq  7759  ltanqg  7761  ltmnqg  7762  distrnq0  7820  addassnq0  7823  prarloclem5  7861  recexprlem1ssl  7994  recexprlem1ssu  7995  mulasssrg  8119  distrsrg  8120  lttrsr  8123  ltsosr  8125  ltasrg  8131  mulextsr1lem  8141  mulextsr1  8142  axmulass  8234  axdistr  8235  dmdcanap  9046  lt2msq1  9209  lediv2  9215  xaddass2  10255  xlt2add  10265  modqdi  10812  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  swrdspsleq  11422  pfxeq  11451  bdtrilem  11988  xrbdtri  12025  bitsfzo  12705  prmexpb  12912  4sqlem18  13170  mgmsscl  13664  subgabl  14119  rng1zrlem  14241  cnptoprest  15323  ssblps  15509  ssbl  15510  rplogbchbase  16035  rplogbreexp  16038  relogbcxpbap  16050  lgssq  16142  uhgr2edg  16430