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  717  pwundifss  4376  ssdomg  6938  negiso  9110  infrenegsupex  9797  xrnegiso  11781  infxrnegsupex  11782  cos01bnd  12277  cos1bnd  12278  cos2bnd  12279  sin4lt0  12286  egt2lt3  12299  epos  12300  ene1  12304  eap1  12305  slotslfn  13066  strslfvd  13082  strslfv2d  13083  strsl0  13089  setsslid  13091  setsslnid  13092  sravscag  14415  reeff1o  15455  pigt2lt4  15466  pire  15468  pipos  15470  sinhalfpi  15478  tan4thpi  15523  sincos3rdpi  15525  pigt3  15526  lgsdir2lem4  15718  lgsdir2lem5  15719