Theorem pm5.74i 236

Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)

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

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bitrd  244  imbi2i  303  bibi2d  309  ibib  331  ibibr  332  anclb  530  pm5.42  531  ancrb  533  cador  1391  cadan  1392  ax12bOLD  1690  equsalhw  1838  equsalhwOLD  1839  equsal  1960  sb6a  2116  ralbiia  2647  clos1induct  5881