Theorem simp1i 1139

Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis

Ref	Expression
3simp1i.1	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Assertion

Ref	Expression
simp1i	⊢ 𝜑

Proof of Theorem simp1i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
2		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  find  7825  hartogslem2  9429  harwdom  9477  divalglem6  16306  structfn  17064  strleun  17065  oppcbas  17621  rescbas  17733  rescabs  17737  rmodislmod  20861  sratset  21115  srads  21117  tngsca  24558  birthday  26889  divsqrsumf  26916  emcl  26938  lgslem4  27236  lgscllem  27240  lgsdir2lem2  27262  mulog2sumlem1  27470  siilem2  30827  h2hva  30949  h2hsm  30950  elunop2  31988  zlmds  33970  zlmtset  33971  wallispilem3  46104  wallispilem4  46105  prstcbas  49585  cnelsubclem  49634