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  849  dcfromcon  1469  dcfrompeirce  1470  nfbii  1497  sbi2v  1917  sbim  1982  sb8mo  2069  cbvmo  2095  necon4ddc  2450  raleqbii  2520  rmo5  2729  cbvrmo  2741  ss2ab  3269  snsssn  3815  trint  4173  ssextss  4282  ordsoexmid  4628  zfregfr  4640  tfi  4648  peano2  4661  peano5  4664  relop  4846  dmcosseq  4969  cotr  5083  issref  5084  cnvsym  5085  intasym  5086  intirr  5088  codir  5090  qfto  5091  cnvpom  5244  cnvsom  5245  funcnvuni  5362  poxp  6341  infmoti  7156  dfinfre  9064  bezoutlembi  12441  algcvgblem  12486  isprm2  12554  ntreq0  14719  ss1oel2o  16127