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  4380  ssdomg  6947  negiso  9128  infrenegsupex  9821  xrnegiso  11816  infxrnegsupex  11817  cos01bnd  12312  cos1bnd  12313  cos2bnd  12314  sin4lt0  12321  egt2lt3  12334  epos  12335  ene1  12339  eap1  12340  slotslfn  13101  strslfvd  13117  strslfv2d  13118  strsl0  13124  setsslid  13126  setsslnid  13127  sravscag  14450  reeff1o  15490  pigt2lt4  15501  pire  15503  pipos  15505  sinhalfpi  15513  tan4thpi  15558  sincos3rdpi  15560  pigt3  15561  lgsdir2lem4  15753  lgsdir2lem5  15754