Theorem imbi12i 239

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 226	. 2 |- ( ( ph -> ch ) <-> ( ph -> th ) )
3		imbi12i.1	. . 3 |- ( ph <-> ps )
4	3	imbi1i 238	. 2 |- ( ( ph -> th ) <-> ( ps -> th ) )
5	2, 4	bitri 184	1 |- ( ( ph -> ch ) <-> ( ps -> th ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stdcn  848  nfbii  1484  sbi2v  1904  sbim  1969  sb8mo  2056  cbvmo  2082  necon4ddc  2436  raleqbii  2506  rmo5  2714  cbvrmo  2725  ss2ab  3247  snsssn  3787  trint  4142  ssextss  4249  ordsoexmid  4594  zfregfr  4606  tfi  4614  peano2  4627  peano5  4630  relop  4812  dmcosseq  4933  cotr  5047  issref  5048  cnvsym  5049  intasym  5050  intirr  5052  codir  5054  qfto  5055  cnvpom  5208  cnvsom  5209  funcnvuni  5323  poxp  6285  infmoti  7087  dfinfre  8975  bezoutlembi  12142  algcvgblem  12187  isprm2  12255  ntreq0  14300  ss1oel2o  15484