Theorem simp1i 1140

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 1137	. 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  find  7839  hartogslem2  9451  harwdom  9499  divalglem6  16358  structfn  17117  strleun  17118  oppcbas  17675  rescbas  17787  rescabs  17791  rmodislmod  20916  sratset  21170  srads  21172  tngsca  24620  birthday  26931  divsqrsumf  26958  emcl  26980  lgslem4  27277  lgscllem  27281  lgsdir2lem2  27303  mulog2sumlem1  27511  siilem2  30938  h2hva  31060  h2hsm  31061  elunop2  32099  zlmds  34122  zlmtset  34123  wallispilem3  46513  wallispilem4  46514  prstcbas  50041  cnelsubclem  50090