Theorem pm3.26bda 422

Description: Deduction eliminating a conjunct.

Hypothesis

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

Assertion

Ref	Expression
pm3.26bda	|- ((ph /\ ps) -> ch)

Proof of Theorem pm3.26bda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 |- (ph -> (ps <-> (ch /\ th)))
2	1	biimpa 418	. 2 |- ((ph /\ ps) -> (ch /\ th))
3	2	pm3.26d 321	1 |- ((ph /\ ps) -> ch)

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

This theorem is referenced by:  climcl 6978  ivthlem1 7281  tg1t 7619  cldss 7668  cnf 7759  cnpf 7760  opnss 7860  caufss 7947  sspnv 8381  lnof 8412  bloln 8440  ubthlem2 8526  fmamo 10727

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