Theorem pm5.74i 587

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 586	. 2 |- ((ph -> (ps <-> ch)) <-> ((ph -> ps) <-> (ph -> ch)))
3	1, 2	mpbi 187	1 |- ((ph -> ps) <-> (ph -> ch))

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

This theorem is referenced by:  mpbidi 592  ibib 593  pm5.42 655  equsal 1188  sb6a 1376  ralbiia 1719  dfom2 3220  weinxp 3319  abfii2 4705  kmlem8 4918  kmlem13 4923  kmlem14 4924  uzindOLD 6379  axgroth2 9050  hgrablkcard 12200

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 145  df-an 223

Copyright terms: Public domain