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  847  nfbii  1473  sbi2v  1892  sbim  1953  sb8mo  2040  cbvmo  2066  necon4ddc  2419  raleqbii  2489  rmo5  2693  cbvrmo  2704  ss2ab  3225  snsssn  3763  trint  4118  ssextss  4222  ordsoexmid  4563  zfregfr  4575  tfi  4583  peano2  4596  peano5  4599  relop  4779  dmcosseq  4900  cotr  5012  issref  5013  cnvsym  5014  intasym  5015  intirr  5017  codir  5019  qfto  5020  cnvpom  5173  cnvsom  5174  funcnvuni  5287  poxp  6235  infmoti  7029  dfinfre  8915  bezoutlembi  12008  algcvgblem  12051  isprm2  12119  ntreq0  13717  ss1oel2o  14828