Theorem pm3.26i 327

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

Syntax hints:   /\ wa 230

This theorem is referenced by:  ssid 2131  ersym 4330  ssdomg 4469  xpmapenlem3 4563  xpmapenlem5 4565  ssrankr1 4738  pre-axlttri 5352  pre-axlttrn 5353  mulnzcnopr 5767  div11 5822  recrec 5834  climunii 7188  caucvg3 7258  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  isumspliti 7306  expcnvlem2 7318  expcnvlem4 7320  geolim 7327  geolim1 7329  negfcncfi 7359  ivthlem4 7374  ivthlem5 7375  ivthlem6 7376  ivthlem7 7377  ivthlem8 7378  ivthlem9 7379  isupivthi 7380  dsupivthlem 7381  efseq1ex 7396  erelem4 7412  ele3lem 7416  ege2le3lem2 7419  absef01tlubi 7478  eirrlem2 7480  eflegeolem2 7505  efcnlem4 7513  reeff1olem2 7516  reeff1o 7517  cos01bndlem3 7563  cos1bnd 7566  cos2bnd 7567  sin4lt0 7573  infunabs 7657  infcdaabs 7658  unctb 7669  bcth 8117  ghgrpilem1 8217  ghgrpilem2 8218  ghgrpilem3 8219  ghgrpilem4 8220  sinco 8750  cosco 8751  pilem1 8754  pilem2 8755  pilem3 8756  sinhalfpi 8763  efifolem1 8805  h2hsm 8927  normlem7tALT 9068  hlimuniii 9191  hhsssh 9222  projlem7 9275  omlsi 9329  shintcli 9376  chintcli 9378  qlaxr3i 9660  lnophm 10027  nmcopex 10042  nmcoplb 10043  nmbdfnlbi 10061  nmcfnex 10071  nmcfnlb 10072  hmopidmchlem 10161  hmopidmchi 10162  hmopidmpji 10163  irred 10406  ghomgrpilem2 10471

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 154  df-an 232

Copyright terms: Public domain