Theorem simp1l 1006

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

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

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

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

This theorem is referenced by:  simpl1l  1033  simpr1l  1039  simp11l  1093  simp21l  1099  simp31l  1105  en2lp  4477  tfisi  4509  funprg  5181  nnsucsssuc  6396  ecopovtrn  6534  ecopovtrng  6537  addassnqg  7214  distrnqg  7219  ltsonq  7230  ltanqg  7232  ltmnqg  7233  distrnq0  7291  addassnq0  7294  mulasssrg  7590  distrsrg  7591  lttrsr  7594  ltsosr  7596  ltasrg  7602  mulextsr1lem  7612  mulextsr1  7613  axmulass  7705  axdistr  7706  dmdcanap  8506  lt2msq1  8667  ltdiv2  8669  lediv2  8673  xaddass  9682  xaddass2  9683  xlt2add  9693  modqdi  10196  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  resqrtcl  10833  bdtrilem  11042  bdtri  11043  xrbdtri  11077  prmexpb  11865  cnptoprest  12447  ssblps  12633  ssbl  12634  rplogbchbase  13075  rplogbreexp  13078  relogbcxpbap  13090