Theorem pm5.74i 583

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

Hypothesis

Ref	Expression
pm5.74i.1	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem pm5.74i

Step	Hyp	Ref	Expression
1		pm5.74i.1	. 2 |- (ph -> (ps <-> ch))
2		pm5.74 582	. 2 |- ((ph -> (ps <-> ch)) <-> ((ph -> ps) <-> (ph -> ch)))
3	1, 2	mpbi 189	1 |- ((ph -> ps) <-> (ph -> ch))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  mpbidi 588  ibib 589  pm5.42 651  equsal 1149  sb6a 1335  ralbiia 1670  dfom2 3128  weinxp 3228  abfii2 4542  kmlem8 4752  kmlem13 4757  kmlem14 4758  uzindOLD 6164  axgroth2 8717  hgrablkcard 10646

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