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 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  7935  hartogslem2  9612  harwdom  9660  divalglem6  16446  structfn  17203  strleun  17204  oppcbas  17777  rescbas  17890  rescabs  17896  rmodislmod  20950  rmodislmodOLD  20951  sratset  21211  srads  21214  tngsca  24683  birthday  27015  divsqrsumf  27042  emcl  27064  lgslem4  27362  lgscllem  27366  lgsdir2lem2  27388  mulog2sumlem1  27596  siilem2  30884  h2hva  31006  h2hsm  31007  elunop2  32045  zlmds  33908  zlmtset  33910  wallispilem3  45988  wallispilem4  45989  prstcbas  48734