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  713  pwundifss  4321  ssdomg  6846  negiso  9001  infrenegsupex  9687  xrnegiso  11446  infxrnegsupex  11447  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  sin4lt0  11951  egt2lt3  11964  epos  11965  ene1  11969  eap1  11970  slotslfn  12731  strslfvd  12747  strslfv2d  12748  strsl0  12754  setsslid  12756  setsslnid  12757  sravscag  14077  reeff1o  15117  pigt2lt4  15128  pire  15130  pipos  15132  sinhalfpi  15140  tan4thpi  15185  sincos3rdpi  15187  pigt3  15188  lgsdir2lem4  15380  lgsdir2lem5  15381