Theorem pm3.27d 323

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.27d.1	|- (ph -> (ps /\ ch))

Assertion

Ref	Expression
pm3.27d	|- (ph -> ch)

Proof of Theorem pm3.27d

Step	Hyp	Ref	Expression
1		pm3.27d.1	. 2 |- (ph -> (ps /\ ch))
2		pm3.27 321	. 2 |- ((ps /\ ch) -> ch)
3	1, 2	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  pm3.27bi 324  pm3.27bda 421  3simp2 795  3simp3 796  nic-mp 967  nic-mpALT 968  sbf 1223  hbs1f 1226  potr 2924  so 2943  nnlim 3231  fcoi2 3753  feu 3754  fcnvres 3755  fv3 3844  ndmord 4111  caoprmo 4131  curry1 4193  curry2 4196  eceqopreq 4454  sdomtr 4619  xpmapenlem5 4647  isfinite2 4692  fin2inf 4693  suplub 4724  infeq5 4766  elom3 4777  r1rankid 4840  unxpdom 4994  sucxpdom 4996  sdomsdomcard 4998  recclpq 5226  ltexpq 5234  ltexpq2 5235  prnmax 5253  prlem934 5293  ltexprlem6 5301  ltexpri 5303  prlem936 5309  reclem3pr 5312  reclem4pr 5313  recexpr 5314  suplem2pr 5316  recexsrlem 5366  addgt0sr 5367  mulgt0sr 5368  mappsrpr 5372  map2psrpr 5374  suppsr2 5377  suppsr3 5378  supsrlem1 5379  nnind 6082  recnz 6362  uzind 6376  uzwo3lem1 6388  flltp1 6428  sqrlem12 6885  sqrlem13 6886  rimul 6945  crim 6971  serzrelem 7264  iserzshft2i 7310  climaddlem3 7319  climmullem5 7327  climmullem8 7330  climabslem 7351  iserzabslem 7381  cvgcmpi 7388  cvgcmpubi 7389  geoisumr 7448  ivthlem6 7491  ivthlem7 7492  efcn 7631  addsin 7665  subsin 7666  addcos 7667  subcos 7668  sin01bndlem3 7678  cos01bndlem3 7680  acdc2lem2 7701  acdc5lem2 7704  inopn 7812  cctop 7862  meteq0 8022  mettri2 8023  mettri4 8024  metxplem2 8037  metxplem4 8043  metxp 8044  tgbl 8081  xplmi 8184  bcthlem13 8222  bcthlem14 8223  bcthlem16 8225  bcthlem17 8226  bcthlem18 8227  bcthlem19 8228  bcthlem20 8229  bcthlem21 8230  bcthlem24 8233  bcthlem25 8234  bcthlem26 8235  grpinv 8286  grprinv 8288  ghgrpilem4 8377  ringsm 8384  ringid 8386  ringdi 8388  ringdir 8389  ringass 8390  vacnlem3 8584  sin2kpi 8955  hlimveci 9334  sh0 9360  shmulcl 9363  shmulclOLD 9364  projlem26 9487  nmcopexlem5 10234  nmcfnexlem5 10263  elpjrn 10398  hstosum 10429  stge0 10432  stle1 10433  stj 10443  ghomlin 10678  ghomgsg 10680  ghomf1olem 10681  unmnd 10951  ununr 10955  uznzr 10967  filusb 11074  cnvtr 11161  cmppfa 11186  rcmob 11203  dmrngcmp 11205  iri 11255  idcvvidc 11293  fmp 11294  reconnlem3 11509  reconnlem4 11510  fcluscf 11724  flimfnfcls 11727  dirdm 11751  dirref 11752  dirtr 11753  dirge 11754  fimax 11837  heiborlem35 12045  hgrablkconn 12198

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 145  df-an 223

Copyright terms: Public domain