Theorem pm3.26bi 329

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	biimpi 158	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.26d 328	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230

This theorem is referenced by:  3simpa 797  pssss 2194  eldifi 2213  inss1 2281  pwssun 2883  sopo 2907  wefr 2996  ordtr 3019  omsson 3193  relop 3332  dmcoss 3420  opres 3432  funrel 3590  fnfun 3642  ffn 3684  f1f 3722  f1of1 3745  f1ofo 3752  nfvres 3805  dff2 3874  isof1o 3951  eqop 4162  xpopth 4164  1st2nd 4166  sdomdom 4447  mapxpen 4560  xpmapenlem3 4563  xpmapenlem4 4564  xpmapenlem5 4565  inf3lemd 4674  rankpw 4746  aceq3lem 4794  aceq5lem4 4800  cardinfima 4956  suppsr3 5289  eqlei 5647  zre 6221  nnssz 6233  dfuzi 6287  uzwo3lem2 6302  sqrlem12 6774  sqrlem13 6775  iserzshft2i 7197  mulc1cncf 7369  ivthlem6 7376  ivthlem7 7377  haustop 7871  cmsmet 8046  xplmi 8058  xplmi2 8059  oprcn 8062  bopcnlem2 8067  bopcnlem3 8068  fsumcnlem 8074  ablgrp 8186  nmogtmnf 8517  bnnv 8610  hlbn 8676  pilem2 8755  pilem3 8756  eff1i 8827  effoi 8828  hcauseq 9135  hlimseqi 9140  hlimveci 9141  shss 9162  sh0 9167  projlem21 9289  projlem26 9294  projlem29 9297  projlem30 9298  lnopf 9868  bdopln 9871  nmopgtmnf 9878  hmopf 9884  lnfnf 9894  unopf1o 9923  elunop2 10021  rnbra 10123  elpjhmop 10196  stcl 10227  stge0 10235  stle1 10236  stcltrlem1 10287  mdslle1i 10328  mdslle2i 10329  filintf 10662

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