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  4552  tfisi  4585  funprg  5265  nnsucsssuc  6490  ecopovtrn  6629  ecopovtrng  6632  addassnqg  7378  distrnqg  7383  ltsonq  7394  ltanqg  7396  ltmnqg  7397  distrnq0  7455  addassnq0  7458  mulasssrg  7754  distrsrg  7755  lttrsr  7758  ltsosr  7760  ltasrg  7766  mulextsr1lem  7776  mulextsr1  7777  axmulass  7869  axdistr  7870  dmdcanap  8675  lt2msq1  8838  ltdiv2  8840  lediv2  8844  xaddass  9865  xaddass2  9866  xlt2add  9876  modqdi  10387  expaddzaplem  10558  expaddzap  10559  expmulzap  10561  resqrtcl  11031  bdtrilem  11240  bdtri  11241  xrbdtri  11277  prmexpb  12143  opprringbg  13181  cnptoprest  13610  ssblps  13796  ssbl  13797  rplogbchbase  14239  rplogbreexp  14242  relogbcxpbap  14254  lgssq  14312