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  4316  ssdomg  6832  negiso  8974  infrenegsupex  9659  xrnegiso  11405  infxrnegsupex  11406  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  sin4lt0  11910  egt2lt3  11923  epos  11924  ene1  11928  eap1  11929  slotslfn  12644  strslfvd  12660  strslfv2d  12661  strsl0  12667  setsslid  12669  setsslnid  12670  sravscag  13939  reeff1o  14908  pigt2lt4  14919  pire  14921  pipos  14923  sinhalfpi  14931  tan4thpi  14976  sincos3rdpi  14978  pigt3  14979  lgsdir2lem4  15147  lgsdir2lem5  15148