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  855  dcfromcon  1494  dcfrompeirce  1495  nfbii  1522  sbi2v  1943  sbim  2009  sb8mo  2096  cbvmo  2122  necon4ddc  2486  raleqbii  2556  rmo5  2767  cbvrmo  2779  ss2ab  3310  snsssn  3870  trint  4228  ssextss  4341  ordsoexmid  4689  zfregfr  4701  tfi  4709  peano2  4722  peano5  4725  relop  4910  dmcosseq  5034  cotr  5149  issref  5150  cnvsym  5151  intasym  5152  intirr  5154  codir  5156  qfto  5157  cnvpom  5310  cnvsom  5311  funcnvuni  5430  poxp  6441  infmoti  7332  dfinfre  9247  bezoutlembi  12726  algcvgblem  12771  isprm2  12839  ntreq0  15123  ss1oel2o  16887