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  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  3881  trint  4239  ssextss  4355  ordsoexmid  4704  zfregfr  4716  tfi  4724  peano2  4737  peano5  4740  relop  4925  dmcosseq  5049  cotr  5164  issref  5165  cnvsym  5166  intasym  5167  intirr  5169  codir  5171  qfto  5172  cnvpom  5325  cnvsom  5326  funcnvuni  5445  poxp  6458  infmoti  7358  dfinfre  9276  bezoutlembi  12760  algcvgblem  12805  isprm2  12873  ntreq0  15156  ss1oel2o  16931