Theorem pm5.74i 584

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 583	. 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 589  ibib 590  pm5.42 652  equsal 1151  sb6a 1337  ralbiia 1673  dfom2 3133  weinxp 3233  abfii2OLD 4562  kmlem8 4772  kmlem13 4777  kmlem14 4778  uzindOLD 6208  axgroth2 8778  hgrablkcard 10774

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