Theorem pm5.74i 644

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

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

This theorem is referenced by:  mpbidi 649  ibib 650  pm5.42 714  equsal 1511  equsalOLD 1512  sb6a 1727  ralbiia 2133  dfom2 3951  weinxp 4059  abfii2 5652  kmlem8 5934  kmlem13 5939  kmlem14 5940  uzindOLD 7420  axgroth2 10133  bnj1171 13439  bnj1253 13470  bnj1283 13476  hgrablkcard 16296

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 164  df-an 242

Copyright terms: Public domain