Theorem simp1l 1021

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1018	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

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

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 980

This theorem is referenced by:  simpl1l  1048  simpr1l  1054  simp11l  1108  simp21l  1114  simp31l  1120  en2lp  4555  tfisi  4588  funprg  5268  nnsucsssuc  6495  ecopovtrn  6634  ecopovtrng  6637  addassnqg  7383  distrnqg  7388  ltsonq  7399  ltanqg  7401  ltmnqg  7402  distrnq0  7460  addassnq0  7463  mulasssrg  7759  distrsrg  7760  lttrsr  7763  ltsosr  7765  ltasrg  7771  mulextsr1lem  7781  mulextsr1  7782  axmulass  7874  axdistr  7875  dmdcanap  8681  lt2msq1  8844  ltdiv2  8846  lediv2  8850  xaddass  9871  xaddass2  9872  xlt2add  9882  modqdi  10394  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  resqrtcl  11040  bdtrilem  11249  bdtri  11250  xrbdtri  11286  prmexpb  12153  opprringbg  13255  cnptoprest  13778  ssblps  13964  ssbl  13965  rplogbchbase  14407  rplogbreexp  14410  relogbcxpbap  14422  lgssq  14480