Theorem simpli 110

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

Syntax hints:   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-ia1 105

This theorem is referenced by:  bi1  117  bi2  129  dfbi2  386  orc  702  pwundifss  4215  ssdomg  6680  negiso  8737  infrenegsupex  9416  xrnegiso  11063  infxrnegsupex  11064  cos01bnd  11501  cos1bnd  11502  cos2bnd  11503  sin4lt0  11509  egt2lt3  11522  epos  11523  ene1  11527  eap1  11528  slotslfn  12024  strslfvd  12039  strslfv2d  12040  strsl0  12046  setsslid  12048  setsslnid  12049  reeff1o  12902  pigt2lt4  12913  pire  12915  pipos  12917  sinhalfpi  12925  tan4thpi  12970  sincos3rdpi  12972  pigt3  12973