Theorem simp1r 1023

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

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

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 981

This theorem is referenced by:  simpl1r  1050  simpr1r  1056  simp11r  1110  simp21r  1116  simp31r  1122  vtoclgft  2799  en2lp  4565  funprg  5278  nnsucsssuc  6507  ecopovtrn  6646  ecopovtrng  6649  addassnqg  7395  distrnqg  7400  ltsonq  7411  ltanqg  7413  ltmnqg  7414  distrnq0  7472  addassnq0  7475  prarloclem5  7513  recexprlem1ssl  7646  recexprlem1ssu  7647  mulasssrg  7771  distrsrg  7772  lttrsr  7775  ltsosr  7777  ltasrg  7783  mulextsr1lem  7793  mulextsr1  7794  axmulass  7886  axdistr  7887  dmdcanap  8693  lt2msq1  8856  lediv2  8862  xaddass2  9884  xlt2add  9894  modqdi  10406  expaddzaplem  10577  expaddzap  10578  expmulzap  10580  bdtrilem  11261  xrbdtri  11298  prmexpb  12165  mgmsscl  12799  subgabl  13167  cnptoprest  14035  ssblps  14221  ssbl  14222  rplogbchbase  14664  rplogbreexp  14667  relogbcxpbap  14679  lgssq  14737