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  4373  ssdomg  6920  negiso  9090  infrenegsupex  9777  xrnegiso  11759  infxrnegsupex  11760  cos01bnd  12255  cos1bnd  12256  cos2bnd  12257  sin4lt0  12264  egt2lt3  12277  epos  12278  ene1  12282  eap1  12283  slotslfn  13044  strslfvd  13060  strslfv2d  13061  strsl0  13067  setsslid  13069  setsslnid  13070  sravscag  14392  reeff1o  15432  pigt2lt4  15443  pire  15445  pipos  15447  sinhalfpi  15455  tan4thpi  15500  sincos3rdpi  15502  pigt3  15503  lgsdir2lem4  15695  lgsdir2lem5  15696