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  4432  ssdomg  7071  negiso  9294  infrenegsupex  10010  xrnegiso  12053  infxrnegsupex  12054  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sin4lt0  12559  egt2lt3  12572  epos  12573  ene1  12577  eap1  12578  slotslfn  13436  strslfvd  13452  strslfv2d  13453  strsl0  13459  setsslid  13461  setsslnid  13462  slotm  13473  sravscag  14889  reeff1o  16032  pigt2lt4  16044  pire  16046  pipos  16048  sinhalfpi  16056  tan4thpi  16101  sincos3rdpi  16103  pigt3  16104  logdivlt  16157  ppiublem1  16324  chtqub  16329  bposlem7  16350  lgsdir2lem4  16388  lgsdir2lem5  16389