Theorem pm3.26i 320

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

Syntax hints:   /\ wa 223

This theorem is referenced by:  ssid 2051  ersym 4210  ssdomg 4343  xpmapenlem3 4430  xpmapenlem5 4432  ssrankr1 4600  pre-axlttri 5210  pre-axlttrn 5211  mulnzcnopr 5622  div11t 5672  recrect 5683  climunii 6986  caucvg3t 7055  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  isumsplit 7102  expcnvlem2 7114  expcnvlem4 7116  geolim 7123  geolim1 7125  negfcncf 7155  ivthlem4 7170  ivthlem5 7171  ivthlem6 7172  ivthlem7 7173  ivthlem8 7174  ivthlem9 7175  isupivth 7176  dsupivthlem 7177  ivthlem4OLD 7179  ivthlem5OLD 7180  ivthlem6OLD 7181  ivthlem7OLD 7182  ivthlem8OLD 7183  ivthOLD 7184  ivth2OLD 7185  efseq1ex 7199  erelem4 7215  ele3lem 7219  ege2le3lem2 7222  absef01tlub 7280  eirrlem2 7282  eflegeolem2 7305  efcnlem4 7313  reeff1olem2 7316  reeff1olem2OLD 7318  reeff1o 7319  cos01bndlem3 7364  cos1bnd 7367  cos2bnd 7368  sin4lt0 7374  infunabs 7459  infcdaabs 7460  unctb 7470  bcth 7914  ghgrpilem1 8018  ghgrpilem2 8019  ghgrpilem3 8020  ghgrpilem4 8021  sinco 8499  cosco 8500  pilem1 8503  pilem2 8504  pilem3 8505  sinhalfpi 8512  efifolem1 8550  ghomgrpilem2 8653  normlem7tALT 9134  hlimunii 9259  projlem7 9322  omls 9375  shintcl 9422  chintcl 9424  qlaxr3 9708  lnophmt 10073  nmcopext 10088  nmcoplbt 10089  nmbdfnlb 10107  nmcfnext 10117  nmcfnlbt 10118  hmopidmchlem 10203  hmopidmch 10204  hmopidmpj 10205  irredt 10444

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