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  7369  dfinfre  9289  bezoutlembi  12801  algcvgblem  12846  isprm2  12914  ntreq0  15324  ss1oel2o  17183  alsbii  17308  ralsbii  17309  alseubii  17340  ralseubii  17341