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 4280  xpmapenlem3 4504  xpmapenlem5 4506  div11t 5766  recrect 5778  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 7472  cos1bnd 7475  cos2bnd 7476  sincos2sgn 7481  sin4lt0 7482  ruclem23 7533  qdensere 7748  bcth 8029  ghgrpilem1 8129  ghgrpilem2 8130  ghgrpilem3 8131  ghgrpilem4 8132  sinco 8662  cosco 8663  pilem2 8667  pilem3 8668  pigt2lt4 8670  sinhalfpilem 8674  coshalfpi 8676  sincosq1lem 8698  sincos4thpi 8705  sincos6thpi 8706  efghgrpilem 8714  efifolem1 8717  logrn 8746  logltbt 8771  h2hsm 8839  normlem7tALT 8980  hlimunii 9103  hhsssh 9134  projlem7 9187  omls 9241  shintcl 9288  chintcl 9290  qlaxr3 9572  lnophmt 9939  nmcopext 9954  nmcoplbt 9955  nmbdfnlb 9973  nmcfnext 9983  nmcfnlbt 9984  hmopidmchlem 10073  hmopidmpj 10075  irredt 10317  ghomgrpilem1 10380

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