Theorem simp1r 1046

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

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

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 1004

This theorem is referenced by:  simpl1r  1073  simpr1r  1079  simp11r  1133  simp21r  1139  simp31r  1145  vtoclgft  2851  en2lp  4647  funprg  5374  nnsucsssuc  6651  ecopovtrn  6792  ecopovtrng  6795  addassnqg  7585  distrnqg  7590  ltsonq  7601  ltanqg  7603  ltmnqg  7604  distrnq0  7662  addassnq0  7665  prarloclem5  7703  recexprlem1ssl  7836  recexprlem1ssu  7837  mulasssrg  7961  distrsrg  7962  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1lem  7983  mulextsr1  7984  axmulass  8076  axdistr  8077  dmdcanap  8885  lt2msq1  9048  lediv2  9054  xaddass2  10083  xlt2add  10093  modqdi  10631  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  swrdspsleq  11220  pfxeq  11249  bdtrilem  11771  xrbdtri  11808  bitsfzo  12487  prmexpb  12694  4sqlem18  12952  mgmsscl  13415  subgabl  13890  cnptoprest  14934  ssblps  15120  ssbl  15121  rplogbchbase  15645  rplogbreexp  15648  relogbcxpbap  15660  lgssq  15740  uhgr2edg  16025