Theorem pm3.26i 345

Description: Inference eliminating a conjunct.

Hypothesis

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

Assertion

Ref	Expression
pm3.26i	|- ph

Proof of Theorem pm3.26i

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

Syntax hints:   /\ wa 239

This theorem is referenced by:  ssidOLD 2468  oeoa 5083  oeoe 5085  ersym 5141  ssdomg 5278  xpmapenlem3 5402  xpmapenlem5 5404  ssrankr1 5596  pre-axlttri 6236  pre-axlttrn 6237  mulnzcnopr 6687  div11 6737  recrec 6748  climunii 8153  caucvg3 8223  cvgcmp3cetlem1 8244  cvgcmp3cetlem2 8245  isumspliti 8272  expcnvlem2 8284  expcnvlem4 8286  geolim 8294  geolim1 8296  negfcncfi 8326  ivthlem4 8341  ivthlem5 8342  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  ivthlem9 8346  isupivthi 8347  dsupivthlem 8348  efseq1ex 8363  erelem4 8379  ele3lem 8383  ege2le3lem2 8386  absef01tlubi 8445  eirrlem2 8447  egt2lt3 8454  eflegeolem2 8474  efcnlem4 8482  reeff1olem2 8485  reeff1o 8486  cos01bndlem3 8532  cos1bnd 8535  cos2bnd 8536  sin4lt0 8542  infunabs 8629  infcdaabs 8630  unctb 8641  bcth 9105  ghgrpilem1 9236  ghgrpilem2 9237  ghgrpilem3 9238  ghgrpilem4 9239  sinco 9811  cosco 9812  pilem1 9815  pilem2 9816  pilem3 9817  sinhalfpi 9824  efifolem1 9871  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  hmopidmchi 11515  hmopidmpji 11516  irred 11759  bnj146 12271  ghomgrpilem2 13421  divalglem5 13492  gcdaddmlem 13526  fsumltisumi 15505  heiborlem42 15678  bfplem6 15685  bfplem7 15686  bfplem11 15690  bfp 15691  stb2xpl 16501  stb3xpl 16502

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