Theorem imbi12i 316

Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12i.1	|- (ph <-> ps)
imbi12i.2	|- (ch <-> th)

Assertion

Ref	Expression
imbi12i	|- ((ph -> ch) <-> (ps -> th))

Proof of Theorem imbi12i

Step	Hyp	Ref	Expression
1		imbi12i.2	. . 3 |- (ch <-> th)
2	1	imbi2i 303	. 2 |- ((ph -> ch) <-> (ph -> th))
3		imbi12i.1	. . 3 |- (ph <-> ps)
4	3	imbi1i 315	. 2 |- ((ph -> th) <-> (ps -> th))
5	2, 4	bitri 240	1 |- ((ph -> ch) <-> (ps -> th))

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

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 177

This theorem is referenced by:  orimdi  820  rb-bijust  1514  nfbii  1569  sb8mo  2223  cbvmo  2241  raleqbii  2645  rmo5  2828  cbvrmo  2835  ss2ab  3335  sscon34  3662  evenodddisjlem1  4516  tfinnn  4535  cotr  5027  cnvsym  5028  intasym  5029  intirr  5030  dffun2  5120  funcnvuni  5162  fvfullfunlem1  5862  clos1induct  5881