Theorem imbi12i 237

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 224	. 2 |- ( ( ph -> ch ) <-> ( ph -> th ) )
3		imbi12i.1	. . 3 |- ( ph <-> ps )
4	3	imbi1i 236	. 2 |- ( ( ph -> th ) <-> ( ps -> th ) )
5	2, 4	bitri 182	1 |- ( ( ph -> ch ) <-> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfbii  1402  sbi2v  1813  sbim  1868  sb8mo  1955  cbvmo  1981  necon4ddc  2317  raleqbii  2378  rmo5  2569  cbvrmo  2576  ss2ab  3062  snsssn  3553  trint  3890  ssextss  3975  ordsoexmid  4305  zfregfr  4316  tfi  4323  peano2  4336  peano5  4339  relop  4504  dmcosseq  4621  cotr  4726  issref  4727  cnvsym  4728  intasym  4729  intirr  4731  codir  4733  qfto  4734  cnvpom  4880  cnvsom  4881  funcnvuni  4988  poxp  5873  infmoti  6441  dfinfre  8034  bezoutlembi  10394  algcvgblem  10431  isprm2  10499