Theorem pm3.27i 324

Description: Inference eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.27i.1	|- (ph /\ ps)

Assertion

Ref	Expression
pm3.27i	|- ps

Proof of Theorem pm3.27i

Step	Hyp	Ref	Expression
1		pm3.27i.1	. 2 |- (ph /\ ps)
2		pm3.27 323	. 2 |- ((ph /\ ps) -> ps)
3	1, 2	ax-mp 7	1 |- ps

Syntax hints:   /\ wa 223

This theorem is referenced by:  ertr 4274  xpmapenlem3 4498  xpmapenlem5 4500  div11t 5765  recrect 5776  faclbnd4lem1 6948  climunii 7098  caucvg3t 7168  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  expcnvlem2 7228  expcnvlem4 7230  geolim 7237  geolim1 7239  negfcncf 7269  ivthlem7 7287  ivthlem8 7288  isupivth 7290  dsupivthlem 7291  efseq1ex 7306  erelem4 7322  erelem5 7323  ele3lem 7326  ege2le3lem1 7327  ege2le3lem2 7329  absef01tlub 7388  eflegeolem2 7414  efm1legeo 7417  efcnlem4 7422  reeff1olem2 7425  reeff1o 7426  cos01bndlem3 7471  cos1bnd 7474  cos2bnd 7475  sincos2sgn 7480  sin4lt0 7481  ruclem23 7532  qdensere 7751  bcth 8032  ghgrpilem1 8133  ghgrpilem2 8134  ghgrpilem3 8135  ghgrpilem4 8136  sinco 8667  cosco 8668  pilem2 8672  pilem3 8673  pigt2lt4 8675  sinhalfpilem 8679  coshalfpi 8681  sincosq1lem 8703  sincos4thpi 8710  sincos6thpi 8711  efghgrpilem 8719  efifolem1 8722  logrn 8751  logltbt 8776  h2hsm 8844  normlem7tALT 8985  hlimunii 9108  hhsssh 9139  projlem7 9192  omls 9246  shintcl 9293  chintcl 9295  qlaxr3 9577  lnophmt 9944  nmcopext 9959  nmcoplbt 9960  nmbdfnlb 9978  nmcfnext 9988  nmcfnlbt 9989  hmopidmchlem 10078  hmopidmpj 10080  irredt 10322  ghomgrpilem1 10385

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain