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 ⊢ 𝜑

This proof depends on syntax axioms:   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia1 106

This theorem is used by:  biimp  118  biimpr  130  dfbi2  392  orc  724  pwundifss  4430  ssdomg  7065  negiso  9288  infrenegsupex  10004  xrnegiso  12046  infxrnegsupex  12047  cos01bnd  12543  cos1bnd  12544  cos2bnd  12545  sin4lt0  12552  egt2lt3  12565  epos  12566  ene1  12570  eap1  12571  slotslfn  13429  strslfvd  13445  strslfv2d  13446  strsl0  13452  setsslid  13454  setsslnid  13455  slotm  13466  sravscag  14831  reeff1o  15926  pigt2lt4  15938  pire  15940  pipos  15942  sinhalfpi  15950  tan4thpi  15995  sincos3rdpi  15997  pigt3  15998  logdivlt  16049  ppiublem1  16213  chtqub  16218  lgsdir2lem4  16272  lgsdir2lem5  16273