Theorem pm3.27d 262

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  pm3.27bd 263  3simp2 595  3simp3 596  sbf 870  hbs1f 874  potr 2134  so 2152  suplub 2161  nnlim 2385  rnexg 2569  fcoi2 2766  feu 2767  fcnvres 2768  fv3 2839  ndmord 3064  caoprmo 3084  eceqopreq 3249  sdomtr 3373  xpmapenlem5 3395  isfinite2 3437  unfi2 3442  inf5 3472  elom3 3478  r1rankid 3537  unxpdom 3650  sucxpdom 3652  sdomsdomcard 3654  recclpq 3866  ltexpq 3874  ltexpq2 3875  prpssnq 3888  prnmax 3893  prlem934 3933  ltexprlem6 3941  ltexpri 3943  prlem936 3949  reclem3pr 3952  reclem4pr 3953  recexpr 3954  suplem2pr 3956  recexsrlem 4006  addgt0sr 4007  mulgt0sr 4008  mappsrpr 4012  map2psrpr 4014  suppsr2 4017  suppsr3 4018  supsrlem1 4019  nnind 4434  nndiv 4453  rimul 4534  uzwo3lem1 4614  flgzt 4626  sqrlem12 4742  sqrlem13 4743  climcn 4879  hlimvec 5110  sh0 5122  projlem26 5218  stge0t 5673  stle1t 5674  stjt 5676

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