Theorem simp1i 1155

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

Syntax hints:   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  find  7888  hartogslem2  9501  harwdom  9549  divalglem6  16452  structfn  17212  strleun  17213  oppcbas  17770  rescbas  17882  rescabs  17886  rmodislmod  21025  sratset  21278  srads  21280  tngsca  24767  birthday  27081  divsqrsumf  27107  emcl  27129  lgslem4  27426  lgscllem  27430  lgsdir2lem2  27452  mulog2sumlem1  27660  siilem2  31141  h2hva  31263  h2hsm  31264  elunop2  32302  zlmds  34293  zlmtset  34294  wallispilem3  46668  wallispilem4  46669  prstcbas  50212  cnelsubclem  50261