Theorem simpli 110

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 108	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-ia1 105

This theorem is referenced by:  biimp  117  biimpr  129  dfbi2  386  orc  702  pwundifss  4263  ssdomg  6744  negiso  8850  infrenegsupex  9532  xrnegiso  11203  infxrnegsupex  11204  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sin4lt0  11707  egt2lt3  11720  epos  11721  ene1  11725  eap1  11726  slotslfn  12420  strslfvd  12435  strslfv2d  12436  strsl0  12442  setsslid  12444  setsslnid  12445  reeff1o  13344  pigt2lt4  13355  pire  13357  pipos  13359  sinhalfpi  13367  tan4thpi  13412  sincos3rdpi  13414  pigt3  13415  lgsdir2lem4  13582  lgsdir2lem5  13583