Theorem pm3.27i 349

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 348	. 2 |- ((ph /\ ps) -> ps)
3	1, 2	ax-mp 7	1 |- ps

Syntax hints:   /\ wa 239

This theorem is referenced by:  oeoa 5083  oeoe 5085  ertr 5143  xpmapenlem3 5402  xpmapenlem5 5404  div11 6737  recrec 6748  faclbnd4lem1 7995  climunii 8153  caucvg3 8223  cvgcmp3cetlem1 8244  cvgcmp3cetlem2 8245  expcnvlem2 8284  expcnvlem4 8286  geolim 8294  geolim1 8296  negfcncfi 8326  ivthlem7 8344  ivthlem8 8345  isupivthi 8347  dsupivthlem 8348  efseq1ex 8363  erelem4 8379  erelem5 8380  ele3lem 8383  ege2le3lem1 8384  ege2le3lem2 8386  absef01tlubi 8445  egt2lt3 8454  eflegeolem2 8474  efm1legeoi 8477  efcnlem4 8482  reeff1olem2 8485  reeff1o 8486  cos01bndlem3 8532  cos1bnd 8535  cos2bnd 8536  sincos2sgn 8541  sin4lt0 8542  ruclem23 8596  bcth 9105  ghgrpilem1 9236  ghgrpilem2 9237  ghgrpilem3 9238  ghgrpilem4 9239  sinco 9811  cosco 9812  pilem2 9816  pilem3 9817  sinhalfpilem 9823  coshalfpi 9825  sincosq1lem 9847  sincos4thpi 9855  sincos6thpi 9856  efghgrpilem 9868  efifolem1 9871  logrn 9900  logltb 9925  h2hsm 10268  normlem7tALT 10410  hlimuniii 10533  hhsssh 10564  projlem7 10617  omlsi 10671  shintcli 10718  chintcli 10720  qlaxr3i 11004  lnophm 11373  nmcopex 11388  nmcoplb 11389  nmbdfnlbi 11407  nmcfnex 11417  nmcfnlb 11418  hmopidmchlem 11514  hmopidmpji 11516  irred 11759  bnj108OLD 12246  bnj146 12271  ghomgrpilem1 13420  divalglem9 13496  fsumltisumi 15505  heiborlem9 15645  heiborlem16 15652  heiborlem40 15676  heiborlem42 15678  bfplem11 15690  bfp 15691  rrncms 15701

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 163  df-an 241

Copyright terms: Public domain