Theorem imbi12i 188

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

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 185	. 2 |- ((ph -> ch) <-> (ph -> th))
3		imbi12i.1	. . 3 |- (ph <-> ps)
4	3	imbi1i 186	. 2 |- ((ph -> th) <-> (ps -> th))
5	2, 4	bitr 173	1 |- ((ph -> ch) <-> (ps -> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  cbvmo 1408  r19.22 1731  ss2ab 2116  prsspw 2480  ssextss 2762  relop 3275  dmcosseq 3365  intasym 3438  cnvpo 3522  funcnvuni 3564  cp 4722  aceq2 4731  kmlem12 4776  kmlem15 4779  zfcndpow 4968  dfinfmr 6067  infmsup 6068  infmxrcl 6086  tgss3t 7638  grothprim 8783  mdsymlem8 10337

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain