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  7874  hartogslem2  9503  harwdom  9551  divalglem6  16375  structfn  17133  strleun  17134  oppcbas  17686  rescbas  17798  rescabs  17802  rmodislmod  20843  sratset  21097  srads  21099  tngsca  24540  birthday  26871  divsqrsumf  26898  emcl  26920  lgslem4  27218  lgscllem  27222  lgsdir2lem2  27244  mulog2sumlem1  27452  siilem2  30788  h2hva  30910  h2hsm  30911  elunop2  31949  zlmds  33959  zlmtset  33960  wallispilem3  46072  wallispilem4  46073  prstcbas  49547  cnelsubclem  49596