Theorem pm3.26bda 420

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 416	. 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 7620  cldss 7671  cnf 7762  cnpf 7763  opnss 7863  caufss 7950  sspnv 8385  lnof 8416  bloln 8444  ubthlem2 8530  fmamo 10756

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