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  1714  equsal  1715  equsalv  1781  sb6a  1976  ralbiia  2480  dfdif3  3232  raaan  3515  exmid01  4177  isprm4  12051