Theorem pm3.27d 325

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 323	. 2 |- ((ps /\ ch) -> ch)
3	1, 2	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.27bi 326  pm3.27bda 421  3simp2 787  3simp3 788  nicodmpraw 950  sbf 1182  hbs1f 1185  potr 2837  so 2855  nnlim 3134  fcoi2 3631  feu 3632  fcnvres 3633  fv3 3718  ndmord 4036  caoprmo 4056  curry1 4082  eceqopreq 4297  sdomtr 4454  xpmapenlem5 4480  isfinite2 4523  fin2inf 4527  suplub 4555  infeq5 4593  elom3 4603  r1rankid 4666  unxpdom 4816  sucxpdom 4818  sdomsdomcard 4820  recclpq 5044  ltexpq 5052  ltexpq2 5053  prnmax 5071  prlem934 5111  ltexprlem6 5119  ltexpri 5121  prlem936 5127  reclem3pr 5130  reclem4pr 5131  recexpr 5132  suplem2pr 5134  recexsrlem 5184  addgt0sr 5185  mulgt0sr 5186  mappsrpr 5190  map2psrpr 5192  suppsr2 5195  suppsr3 5196  supsrlem1 5197  nnind 5885  recnzt 6138  uzind 6153  uzwo3lem1 6164  flltp1t 6177  sqrlem12 6614  sqrlem13 6615  rimul 6675  crimt 6704  crimtOLD 6705  serzrelem 6999  iserzshft2 7044  climaddlem3 7052  climmullem5 7060  climmullem8 7063  climabslem 7084  iserzabslem 7114  cvgcmp 7120  cvgcmpub 7121  geoisumr 7178  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efcn 7363  addsint 7399  subsint 7400  addcost 7401  subcost 7402  sin01bndlem3 7411  cos01bndlem3 7413  acdc2lem2 7431  acdc5lem2 7434  inopnt 7542  fctop 7592  cctop 7594  meteq0 7751  mettri2 7752  mettri4 7753  metxplem2 7767  metxplem4 7773  metxp 7774  tgbl 7811  xplmi 7907  bcthlem13 7945  bcthlem14 7946  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  bcthlem19 7951  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  bcthlem26 7958  grpinv 8003  grprinv 8005  ghgrpilem4 8073  ringsm 8080  ringid 8082  ringdi 8083  ringdir 8084  ringass 8085  sin2kpi 8607  circcltOLD 8656  hlimvec 8979  sh0 9005  shmulclt 9008  shmulcltOLD 9009  projlem26 9127  nmcopexlem5 9870  nmcfnexlem5 9899  elpjrnt 10027  hstosumt 10058  stge0t 10061  stle1t 10062  stjt 10072  ghomlin 10298  ghomgsg 10300  ghomf1olem 10301  osbs 10392  filusb 10436  cnvtr 10482  cmppfa 10509  rcmob 10526  iri 10572  idcvvidc 10597  hgrablkconn 10608

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