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  dcfromcon  1459  dcfrompeirce  1460  nfbii  1487  sbi2v  1907  sbim  1972  sb8mo  2059  cbvmo  2085  necon4ddc  2439  raleqbii  2509  rmo5  2717  cbvrmo  2728  ss2ab  3251  snsssn  3791  trint  4146  ssextss  4253  ordsoexmid  4598  zfregfr  4610  tfi  4618  peano2  4631  peano5  4634  relop  4816  dmcosseq  4937  cotr  5051  issref  5052  cnvsym  5053  intasym  5054  intirr  5056  codir  5058  qfto  5059  cnvpom  5212  cnvsom  5213  funcnvuni  5327  poxp  6290  infmoti  7094  dfinfre  8983  bezoutlembi  12172  algcvgblem  12217  isprm2  12285  ntreq0  14368  ss1oel2o  15638