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 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  find  7889  findOLD  7890  hartogslem2  9540  harwdom  9588  divalglem6  16345  structfn  17093  strleun  17094  oppcbas  17667  rescbas  17780  rescabs  17786  rmodislmod  20684  rmodislmodOLD  20685  sratset  20948  srads  20951  tngsca  24378  birthday  26683  divsqrsumf  26709  emcl  26731  lgslem4  27027  lgscllem  27031  lgsdir2lem2  27053  mulog2sumlem1  27261  siilem2  30360  h2hva  30482  h2hsm  30483  elunop2  31521  zlmds  33228  zlmtset  33230  wallispilem3  45082  wallispilem4  45083  prstcbas  47775