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  707  pwundifss  4270  ssdomg  6756  negiso  8871  infrenegsupex  9553  xrnegiso  11225  infxrnegsupex  11226  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sin4lt0  11729  egt2lt3  11742  epos  11743  ene1  11747  eap1  11748  slotslfn  12442  strslfvd  12457  strslfv2d  12458  strsl0  12464  setsslid  12466  setsslnid  12467  reeff1o  13488  pigt2lt4  13499  pire  13501  pipos  13503  sinhalfpi  13511  tan4thpi  13556  sincos3rdpi  13558  pigt3  13559  lgsdir2lem4  13726  lgsdir2lem5  13727