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  4405  ssdomg  7017  negiso  9228  infrenegsupex  9925  xrnegiso  11943  infxrnegsupex  11944  cos01bnd  12440  cos1bnd  12441  cos2bnd  12442  sin4lt0  12449  egt2lt3  12462  epos  12463  ene1  12467  eap1  12468  slotslfn  13230  strslfvd  13246  strslfv2d  13247  strsl0  13253  setsslid  13255  setsslnid  13256  sravscag  14583  reeff1o  15630  pigt2lt4  15641  pire  15643  pipos  15645  sinhalfpi  15653  tan4thpi  15698  sincos3rdpi  15700  pigt3  15701  lgsdir2lem4  15896  lgsdir2lem5  15897