Theorem simp1r 987

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 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 983	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  simpl1r  1014  simpr1r  1020  simp11r  1074  simp21r  1080  simp31r  1086  vtoclgft  2705  en2lp  4427  funprg  5129  nnsucsssuc  6340  ecopovtrn  6478  ecopovtrng  6481  addassnqg  7132  distrnqg  7137  ltsonq  7148  ltanqg  7150  ltmnqg  7151  distrnq0  7209  addassnq0  7212  prarloclem5  7250  recexprlem1ssl  7383  recexprlem1ssu  7384  mulasssrg  7495  distrsrg  7496  lttrsr  7499  ltsosr  7501  ltasrg  7507  mulextsr1lem  7516  mulextsr1  7517  axmulass  7602  axdistr  7603  dmdcanap  8389  lt2msq1  8547  lediv2  8553  xaddass2  9540  xlt2add  9550  modqdi  10052  expaddzaplem  10223  expaddzap  10224  expmulzap  10226  bdtrilem  10896  xrbdtri  10931  prmexpb  11669  cnptoprest  12244  ssblps  12408  ssbl  12409