Theorem pm5.74i 260

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

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

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 197

This theorem is referenced by:  bitrd  268  imbi2i  326  bibi2d  332  ibib  357  ibibr  358  anclb  570  pm5.42  571  ancrb  573  cador  1547  equsalvw  1931  ax13b  1964  equsalv  2108  equsalhw  2123  equsal  2291  sbcom3  2411  2sb6rf  2452  ralbiia  2979  frinxp  5184  dfom2  7067  dfacacn  8963  kmlem8  8979  kmlem13  8984  kmlem14  8985  axgroth2  9647  rabeqsnd  29342  bnj1171  31068  bnj1253  31085  filnetlem4  32376  bj-ssb1a  32632  bj-ssb1  32633  bj-ssbcom3lem  32650  wl-sbcom3  33372  elintima  37945