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  852  dcfromcon  1491  dcfrompeirce  1492  nfbii  1519  sbi2v  1939  sbim  2004  sb8mo  2091  cbvmo  2117  necon4ddc  2472  raleqbii  2542  rmo5  2752  cbvrmo  2764  ss2ab  3292  snsssn  3839  trint  4197  ssextss  4306  ordsoexmid  4654  zfregfr  4666  tfi  4674  peano2  4687  peano5  4690  relop  4872  dmcosseq  4996  cotr  5110  issref  5111  cnvsym  5112  intasym  5113  intirr  5115  codir  5117  qfto  5118  cnvpom  5271  cnvsom  5272  funcnvuni  5390  poxp  6378  infmoti  7195  dfinfre  9103  bezoutlembi  12526  algcvgblem  12571  isprm2  12639  ntreq0  14806  ss1oel2o  16355