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  4377  ssdomg  6943  negiso  9118  infrenegsupex  9806  xrnegiso  11794  infxrnegsupex  11795  cos01bnd  12290  cos1bnd  12291  cos2bnd  12292  sin4lt0  12299  egt2lt3  12312  epos  12313  ene1  12317  eap1  12318  slotslfn  13079  strslfvd  13095  strslfv2d  13096  strsl0  13102  setsslid  13104  setsslnid  13105  sravscag  14428  reeff1o  15468  pigt2lt4  15479  pire  15481  pipos  15483  sinhalfpi  15491  tan4thpi  15536  sincos3rdpi  15538  pigt3  15539  lgsdir2lem4  15731  lgsdir2lem5  15732