Theorem imbi12i 237

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfbii  1405  sbi2v  1817  sbim  1872  sb8mo  1959  cbvmo  1985  necon4ddc  2323  raleqbii  2386  rmo5  2578  cbvrmo  2585  ss2ab  3078  snsssn  3590  trint  3928  ssextss  4023  ordsoexmid  4353  zfregfr  4364  tfi  4372  peano2  4385  peano5  4388  relop  4556  dmcosseq  4674  cotr  4782  issref  4783  cnvsym  4784  intasym  4785  intirr  4787  codir  4789  qfto  4790  cnvpom  4941  cnvsom  4942  funcnvuni  5050  poxp  5956  infmoti  6670  dfinfre  8355  bezoutlembi  10900  algcvgblem  10937  isprm2  11005  ss1oel2o  11357