Theorem imbi12i 238

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stdcn  837  nfbii  1461  sbi2v  1880  sbim  1941  sb8mo  2028  cbvmo  2054  necon4ddc  2408  raleqbii  2478  rmo5  2681  cbvrmo  2691  ss2ab  3210  snsssn  3741  trint  4095  ssextss  4198  ordsoexmid  4539  zfregfr  4551  tfi  4559  peano2  4572  peano5  4575  relop  4754  dmcosseq  4875  cotr  4985  issref  4986  cnvsym  4987  intasym  4988  intirr  4990  codir  4992  qfto  4993  cnvpom  5146  cnvsom  5147  funcnvuni  5257  poxp  6200  infmoti  6993  dfinfre  8851  bezoutlembi  11938  algcvgblem  11981  isprm2  12049  ntreq0  12772  ss1oel2o  13873