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  720  pwundifss  4411  ssdomg  7031  negiso  9249  infrenegsupex  9947  xrnegiso  11976  infxrnegsupex  11977  cos01bnd  12473  cos1bnd  12474  cos2bnd  12475  sin4lt0  12482  egt2lt3  12495  epos  12496  ene1  12500  eap1  12501  slotslfn  13326  strslfvd  13342  strslfv2d  13343  strsl0  13349  setsslid  13351  setsslnid  13352  sravscag  14721  reeff1o  15768  pigt2lt4  15779  pire  15781  pipos  15783  sinhalfpi  15791  tan4thpi  15836  sincos3rdpi  15838  pigt3  15839  lgsdir2lem4  16034  lgsdir2lem5  16035