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  720  pwundifss  4411  ssdomg  7031  negiso  9246  infrenegsupex  9944  xrnegiso  11972  infxrnegsupex  11973  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  sin4lt0  12478  egt2lt3  12491  epos  12492  ene1  12496  eap1  12497  slotslfn  13322  strslfvd  13338  strslfv2d  13339  strsl0  13345  setsslid  13347  setsslnid  13348  sravscag  14703  reeff1o  15750  pigt2lt4  15761  pire  15763  pipos  15765  sinhalfpi  15773  tan4thpi  15818  sincos3rdpi  15820  pigt3  15821  lgsdir2lem4  16016  lgsdir2lem5  16017