Theorem simp1l 973

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

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

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 932

This theorem is referenced by:  simpl1l  1000  simpr1l  1006  simp11l  1060  simp21l  1066  simp31l  1072  en2lp  4407  tfisi  4439  funprg  5109  nnsucsssuc  6318  ecopovtrn  6456  ecopovtrng  6459  addassnqg  7091  distrnqg  7096  ltsonq  7107  ltanqg  7109  ltmnqg  7110  distrnq0  7168  addassnq0  7171  mulasssrg  7454  distrsrg  7455  lttrsr  7458  ltsosr  7460  ltasrg  7466  mulextsr1lem  7475  mulextsr1  7476  axmulass  7558  axdistr  7559  dmdcanap  8343  lt2msq1  8501  ltdiv2  8503  lediv2  8507  xaddass  9493  xaddass2  9494  xlt2add  9504  modqdi  10006  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  resqrtcl  10641  bdtrilem  10849  bdtri  10850  xrbdtri  10884  prmexpb  11622  cnptoprest  12189  ssblps  12353  ssbl  12354