Theorem imbi12i 163

Description: Join two logical equivalences to form equivalence of implications.

Hypotheses

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

Assertion

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

Proof of Theorem imbi12i

Step	Hyp	Ref	Expression
1		bi2im.2	. . 3 |- (ch <-> th)
2	1	imbi2i 160	. 2 |- ((ph -> ch) <-> (ph -> th))
3		bi2im.1	. . 3 |- (ph <-> ps)
4	3	imbi1i 161	. 2 |- ((ph -> th) <-> (ps -> th))
5	2, 4	bitr 151	1 |- ((ph -> ch) <-> (ps -> th))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  cbvmo 1034  r19.22 1272  ss2ab 1551  prsspw 1858  ssextss 1864  dmcosseq 2572  intasym 2627  funcnvuni 2706  cp 3547  aceq2 3554  kmlem11 3590  kmlem15 3594  zfcndpow 3762  mdsymlem8 5783

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org