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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  stdcn  859  dcfromcon  1498  dcfrompeirce  1499  nfbii  1526  sbi2v  1947  sbim  2013  sb8mo  2100  cbvmo  2126  necon4ddc  2492  raleqbii  2562  rmo5  2773  cbvrmo  2785  ss2ab  3316  snsssn  3886  trint  4244  ssextss  4360  ordsoexmid  4709  zfregfr  4721  tfi  4729  peano2  4742  peano5  4745  relop  4930  dmcosseq  5054  cotr  5169  issref  5170  cnvsym  5171  intasym  5172  intirr  5174  codir  5176  qfto  5177  cnvpom  5330  cnvsom  5331  funcnvuni  5450  poxp  6468  infmoti  7368  dfinfre  9286  bezoutlembi  12782  algcvgblem  12827  isprm2  12895  ntreq0  15233  ss1oel2o  17017  alsbii  17141  ralsbii  17142  alseubii  17173  ralseubii  17174