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 1406  r19.22 1728  ss2ab 2112  prsspw 2476  ssextss 2757  relop 3270  dmcosseq 3357  intasym 3430  cnvpo 3514  funcnvuni 3556  cp 4702  aceq2 4711  kmlem12 4756  kmlem15 4759  zfcndpow 4948  dfinfmr 6022  infmsup 6023  infmxrcl 6041  tgss3t 7588  grothprim 8722  mdsymlem8 10274

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