Theorem pm5.74i 179

Description: Distribution of implication over biconditional (inference form). (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 178	. 2 |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
3	1, 2	mpbi 144	1 |- ( ( ph -> ps ) <-> ( ph -> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitrd  187  imbi2i  225  bibi2d  231  ibib  244  ibibr  245  anclb  317  pm5.42  318  ancrb  320  equsalh  1704  equsal  1705  sb6a  1961  ralbiia  2447  dfdif3  3181  raaan  3464  exmid01  4116  isprm4  11789