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 ⊢ 𝜑

Syntax hints:   ∧ wa 104

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

This theorem is referenced by:  biimp  118  biimpr  130  dfbi2  388  orc  713  pwundifss  4317  ssdomg  6834  negiso  8976  infrenegsupex  9662  xrnegiso  11408  infxrnegsupex  11409  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  sin4lt0  11913  egt2lt3  11926  epos  11927  ene1  11931  eap1  11932  slotslfn  12647  strslfvd  12663  strslfv2d  12664  strsl0  12670  setsslid  12672  setsslnid  12673  sravscag  13942  reeff1o  14949  pigt2lt4  14960  pire  14962  pipos  14964  sinhalfpi  14972  tan4thpi  15017  sincos3rdpi  15019  pigt3  15020  lgsdir2lem4  15188  lgsdir2lem5  15189