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  1403  sbi2v  1814  sbim  1869  sb8mo  1956  cbvmo  1982  necon4ddc  2318  raleqbii  2379  rmo5  2570  cbvrmo  2577  ss2ab  3063  snsssn  3561  trint  3898  ssextss  3983  ordsoexmid  4313  zfregfr  4324  tfi  4331  peano2  4344  peano5  4347  relop  4514  dmcosseq  4631  cotr  4736  issref  4737  cnvsym  4738  intasym  4739  intirr  4741  codir  4743  qfto  4744  cnvpom  4890  cnvsom  4891  funcnvuni  4999  poxp  5884  infmoti  6500  dfinfre  8101  bezoutlembi  10538  algcvgblem  10575  isprm2  10643