Theorem pm5.74i 178

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bitrd  186  imbi2i  224  bibi2d  230  ibib  243  ibibr  244  anclb  312  pm5.42  313  ancrb  315  equsalh  1661  equsal  1662  sb6a  1912  ralbiia  2392  dfdif3  3110  raaan  3388  exmid01  4032  isprm4  11379