Theorem pm5.74da 585

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 584	1 |- (ph -> ((ps -> ch) <-> (ps -> th)))

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

This theorem is referenced by:  ralbida 1654  ordunisuc2 3110  dfom2 3128  suplem2pr 5142  uzindOLD 6164  cau2 6858  metcnplem 7838  cncfmet 7857  dmdbr5at 10284

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