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  7833  hartogslem2  9438  harwdom  9486  divalglem6  16313  structfn  17071  strleun  17072  oppcbas  17628  rescbas  17740  rescabs  17744  rmodislmod  20867  sratset  21121  srads  21123  tngsca  24563  birthday  26894  divsqrsumf  26921  emcl  26943  lgslem4  27241  lgscllem  27245  lgsdir2lem2  27267  mulog2sumlem1  27475  siilem2  30836  h2hva  30958  h2hsm  30959  elunop2  31997  zlmds  33998  zlmtset  33999  wallispilem3  46192  wallispilem4  46193  prstcbas  49682  cnelsubclem  49731