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  1719  equsal  1720  equsalv  1786  sb6a  1981  ralbiia  2484  dfdif3  3237  raaan  3521  exmid01  4184  isprm4  12073