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  714  pwundifss  4337  ssdomg  6880  negiso  9041  infrenegsupex  9728  xrnegiso  11623  infxrnegsupex  11624  cos01bnd  12119  cos1bnd  12120  cos2bnd  12121  sin4lt0  12128  egt2lt3  12141  epos  12142  ene1  12146  eap1  12147  slotslfn  12908  strslfvd  12924  strslfv2d  12925  strsl0  12931  setsslid  12933  setsslnid  12934  sravscag  14255  reeff1o  15295  pigt2lt4  15306  pire  15308  pipos  15310  sinhalfpi  15318  tan4thpi  15363  sincos3rdpi  15365  pigt3  15366  lgsdir2lem4  15558  lgsdir2lem5  15559