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 4258  xpmapenlem3 4478  xpmapenlem5 4480  div11t 5721  recrect 5732  faclbnd4lem1 6885  climunii 7035  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  expcnvlem2 7163  expcnvlem4 7165  geolim 7172  geolim1 7174  negfcncf 7204  ivthlem7 7222  ivthlem8 7223  isupivth 7225  dsupivthlem 7226  ivthlem7OLD 7231  ivthlem8OLD 7232  ivthOLD 7233  efseq1ex 7248  erelem4 7264  erelem5 7265  ele3lem 7268  ege2le3lem1 7269  ege2le3lem2 7271  absef01tlub 7329  eflegeolem2 7354  efm1legeo 7357  efcnlem4 7362  reeff1olem2 7365  reeff1olem2OLD 7367  reeff1o 7368  cos01bndlem3 7413  cos1bnd 7416  cos2bnd 7417  sincos2sgn 7422  sin4lt0 7423  ruclem23 7475  qdensere 7691  bcth 7966  ghgrpilem1 8070  ghgrpilem2 8071  ghgrpilem3 8072  ghgrpilem4 8073  sinco 8586  cosco 8587  pilem2 8591  pilem3 8592  pigt2lt4 8594  sinhalfpilem 8598  coshalfpi 8600  sincosq1lem 8620  sincos4thpi 8627  sincos6thpi 8628  efghgrpilem 8634  efifolem1 8637  logrn 8673  logltbt 8698  logltbtOLD 8715  h2hsm 8783  normlem7tALT 8906  hlimunii 9029  hhsssh 9059  projlem7 9108  omls 9161  shintcl 9208  chintcl 9210  qlaxr3 9494  lnophmt 9859  nmcopext 9874  nmcoplbt 9875  nmbdfnlb 9893  nmcfnext 9903  nmcfnlbt 9904  hmopidmchlem 9989  hmopidmpj 9991  irredt 10230  ghomgrpilem1 10290

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