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  719  pwundifss  4382  ssdomg  6952  negiso  9135  infrenegsupex  9828  xrnegiso  11827  infxrnegsupex  11828  cos01bnd  12324  cos1bnd  12325  cos2bnd  12326  sin4lt0  12333  egt2lt3  12346  epos  12347  ene1  12351  eap1  12352  slotslfn  13113  strslfvd  13129  strslfv2d  13130  strsl0  13136  setsslid  13138  setsslnid  13139  sravscag  14463  reeff1o  15503  pigt2lt4  15514  pire  15516  pipos  15518  sinhalfpi  15526  tan4thpi  15571  sincos3rdpi  15573  pigt3  15574  lgsdir2lem4  15766  lgsdir2lem5  15767