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  7880  hartogslem2  9493  harwdom  9541  divalglem6  16444  structfn  17204  strleun  17205  oppcbas  17762  rescbas  17874  rescabs  17878  rmodislmod  21017  sratset  21270  srads  21272  tngsca  24759  birthday  27073  divsqrsumf  27099  emcl  27121  lgslem4  27418  lgscllem  27422  lgsdir2lem2  27444  mulog2sumlem1  27652  siilem2  31109  h2hva  31231  h2hsm  31232  elunop2  32270  zlmds  34264  zlmtset  34265  wallispilem3  46640  wallispilem4  46641  prstcbas  50184  cnelsubclem  50233