Theorem pm5.74da 586

Description: Distribution of implication over biconditional (deduction rule).

Hypothesis

Ref	Expression
pm5.74da.1	|- ((ph /\ ps) -> (ch <-> th))

Assertion

Ref	Expression
pm5.74da	|- (ph -> ((ps -> ch) <-> (ps -> th)))

Proof of Theorem pm5.74da

Step	Hyp	Ref	Expression
1		pm5.74da.1	. . 3 |- ((ph /\ ps) -> (ch <-> th))
2	1	ex 373	. 2 |- (ph -> (ps -> (ch <-> th)))
3	2	pm5.74d 585	1 |- (ph -> ((ps -> ch) <-> (ps -> th)))

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

This theorem is referenced by:  ralbida 1657  ordunisuc2 3115  dfom2 3133  suplem2pr 5162  uzindOLD 6208  cau2 6913  metcnplem 7886  cncfmet 7905  dmdbr5at 10349

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