Theorem simpli 111

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpli	⊢ 𝜑

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

This proof depends on syntax axioms:   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia1 106

This theorem is used by:  biimp  118  biimpr  130  dfbi2  392  orc  724  pwundifss  4430  ssdomg  7065  negiso  9286  infrenegsupex  9996  xrnegiso  12030  infxrnegsupex  12031  cos01bnd  12527  cos1bnd  12528  cos2bnd  12529  sin4lt0  12536  egt2lt3  12549  epos  12550  ene1  12554  eap1  12555  slotslfn  13380  strslfvd  13396  strslfv2d  13397  strsl0  13403  setsslid  13405  setsslnid  13406  slotm  13417  sravscag  14782  reeff1o  15876  pigt2lt4  15888  pire  15890  pipos  15892  sinhalfpi  15900  tan4thpi  15945  sincos3rdpi  15947  pigt3  15948  logdivlt  15999  lgsdir2lem4  16162  lgsdir2lem5  16163