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 ⊢ 𝜑

This proof depends on syntax axioms:   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia1 106

This theorem is used by:  biimp  118  biimpr  130  dfbi2  392  orc  724  pwundifss  4432  ssdomg  7070  negiso  9294  infrenegsupex  10011  xrnegiso  12054  infxrnegsupex  12055  cos01bnd  12551  cos1bnd  12552  cos2bnd  12553  sin4lt0  12560  egt2lt3  12573  epos  12574  ene1  12578  eap1  12579  slotslfn  13437  strslfvd  13453  strslfv2d  13454  strsl0  13460  setsslid  13462  setsslnid  13463  slotm  13474  sravscag  14890  reeff1o  16011  pigt2lt4  16023  pire  16025  pipos  16027  sinhalfpi  16035  tan4thpi  16080  sincos3rdpi  16082  pigt3  16083  logdivlt  16136  ppiublem1  16303  chtqub  16308  bposlem7  16329  lgsdir2lem4  16367  lgsdir2lem5  16368