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:  biimp  117  biimpr  129  dfbi2  386  orc  702  pwundifss  4247  ssdomg  6725  negiso  8831  infrenegsupex  9510  xrnegiso  11170  infxrnegsupex  11171  cos01bnd  11666  cos1bnd  11667  cos2bnd  11668  sin4lt0  11674  egt2lt3  11687  epos  11688  ene1  11692  eap1  11693  slotslfn  12286  strslfvd  12301  strslfv2d  12302  strsl0  12308  setsslid  12310  setsslnid  12311  reeff1o  13164  pigt2lt4  13175  pire  13177  pipos  13179  sinhalfpi  13187  tan4thpi  13232  sincos3rdpi  13234  pigt3  13235