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  4388  ssdomg  6995  negiso  9178  infrenegsupex  9871  xrnegiso  11883  infxrnegsupex  11884  cos01bnd  12380  cos1bnd  12381  cos2bnd  12382  sin4lt0  12389  egt2lt3  12402  epos  12403  ene1  12407  eap1  12408  slotslfn  13169  strslfvd  13185  strslfv2d  13186  strsl0  13192  setsslid  13194  setsslnid  13195  sravscag  14519  reeff1o  15564  pigt2lt4  15575  pire  15577  pipos  15579  sinhalfpi  15587  tan4thpi  15632  sincos3rdpi  15634  pigt3  15635  lgsdir2lem4  15830  lgsdir2lem5  15831