Theorem pm3.26bd 259

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.26bd.1	|- (ph <-> (ps /\ ch))

Assertion

Ref	Expression
pm3.26bd	|- (ph -> ps)

Proof of Theorem pm3.26bd

Step	Hyp	Ref	Expression
1		pm3.26bd.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimp 133	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.26d 258	1 |- (ph -> ps)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  3simpa 591  pssss 1567  eldifi 1591  inss1 1657  pwssun 1917  sopo 2139  wefr 2191  ordtr 2213  omsson 2377  dmco 2570  opres 2580  funrel 2681  fnfun 2721  ffn 2752  f1f 2781  f1of1 2799  f1ofo 2806  nfvres 2850  isof1o 2931  sdomdom 3290  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  xpmapenlem5 3395  inf3lemd 3463  rankpw 3528  aceq3lem 3555  aceq5lem4 3561  cardinfima 3696  suppsr3 4018  eqle 4304  zret 4567  nnssz 4577  uzwo3lem2 4615  sqrlem12 4742  sqrlem13 4743  climseq 4878  climcn 4879  cauchyseq 5104  hlimseq 5109  hlimvec 5110  shss 5117  sh0 5122  projlem21 5213  projlem26 5218  projlem29 5221  projlem30 5222  stclt 5672  stge0t 5673  stle1t 5674  stcltrlem1 5709

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org