Theorem pm3.26bi 322

Description: Deduction eliminating a conjunct.

Hypothesis

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

Assertion

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

Proof of Theorem pm3.26bi

Step	Hyp	Ref	Expression
1		pm3.26bi.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimp 151	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.26d 321	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  3simpa 785  pssss 2143  eldifi 2162  inss1 2230  pwssun 2827  sopo 2851  wefr 2939  ordtr 2962  omsson 3136  relop 3275  dmcoss 3363  opres 3375  funrel 3533  fnfun 3585  ffn 3627  f1f 3665  f1of1 3688  f1ofo 3695  nfvres 3748  dff2 3817  isof1o 3893  eqop 4104  xpopth 4106  1st2nd 4108  sdomdom 4386  mapxpen 4495  xpmapenlem3 4498  xpmapenlem4 4499  xpmapenlem5 4500  inf3lemd 4612  rankpw 4684  aceq3lem 4732  aceq5lem4 4738  cardinfima 4891  suppsr3 5224  eqle 5582  zret 6139  nnssz 6151  dfuz 6202  uzwo3lem2 6217  sqrlem12 6684  sqrlem13 6685  iserzshft2 7107  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  haustop 7786  cmsmet 7961  xplmi 7973  xplmi2 7974  oprcn 7977  bopcnlem2 7982  bopcnlem3 7983  fsumcnlem 7989  ablgrp 8102  nmogtmnf 8433  bnnv 8526  hlbn 8592  pilem2 8672  pilem3 8673  eff1i 8744  effoi 8745  hcauseq 9052  hlimseq 9057  hlimvec 9058  shss 9079  sh0 9084  projlem21 9206  projlem26 9211  projlem29 9214  projlem30 9215  lnopft 9785  bdoplnt 9788  nmopgtmnf 9795  hmopft 9801  lnfnft 9811  unopf1ot 9840  elunop2t 9938  rnbra 10040  elpjhmopt 10113  stclt 10143  stge0t 10151  stle1t 10152  stcltrlem1 10203  mdslle1 10244  mdslle2 10245  filintf 10569

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