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  2814  en2lp  4591  funprg  5309  nnsucsssuc  6559  ecopovtrn  6700  ecopovtrng  6703  addassnqg  7468  distrnqg  7473  ltsonq  7484  ltanqg  7486  ltmnqg  7487  distrnq0  7545  addassnq0  7548  prarloclem5  7586  recexprlem1ssl  7719  recexprlem1ssu  7720  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  dmdcanap  8768  lt2msq1  8931  lediv2  8937  xaddass2  9964  xlt2add  9974  modqdi  10503  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  bdtrilem  11423  xrbdtri  11460  bitsfzo  12139  prmexpb  12346  4sqlem18  12604  mgmsscl  13065  subgabl  13540  cnptoprest  14583  ssblps  14769  ssbl  14770  rplogbchbase  15294  rplogbreexp  15297  relogbcxpbap  15309  lgssq  15389