Theorem simp1i 1157

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 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  find  7905  hartogslem2  9530  harwdom  9578  divalglem6  16561  structfn  17327  strleun  17328  oppcbas  17885  rescbas  17997  rescabs  18001  rmodislmod  21198  sratset  21451  srads  21453  tngsca  24957  birthday  27275  divsqrsumf  27301  emcl  27323  lgslem4  27620  lgscllem  27624  lgsdir2lem2  27646  mulog2sumlem1  27854  siilem2  31447  h2hva  31569  h2hsm  31570  elunop2  32608  zlmds  34587  zlmtset  34588  wallispilem3  47046  wallispilem4  47047  prstcbas  50631  cnelsubclem  50680