Theorem imbi12i 205

Description: Join two logical equivalences to form equivalence of implications.

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

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  cbvmo 1804  reximOLD 2195  ss2ab 2675  sbsslem 2978  prsspwOLD 3151  trint 3426  ssextss 3507  trsuc2 3754  relop 4113  dmcosseq 4214  dmcosseqOLD 4215  cotr 4302  cnvsym 4304  intasym 4306  intasymOLD 4307  intirr 4312  cnvpo 4427  funcnvuni 4482  ordiso 5683  cp 5852  aceq2 5893  kmlem12 5938  kmlem15 5941  zfcndpow 6120  dfinfmr 7276  infmsup 7277  infmxrcl 7295  tgss3 8908  grothprim 10141  mdsymlem8 11982  bnj24 12388  bnj34 12403  bnj36OLD 12406  bnj37 12407  bnj37OLD 12408  bnj58 12431  bnj82 13210  bnj92 13216  bnj109 13226  bnj539 13266  bnj540 13267  bnj541 13268  bnj1045 13392  bnj1069 13400  bnj1081 13407  bnj1134 13427  algcvgblem 13745  isprm2 13775  axrepprim 13786  axacprim 13791  trsuc2OLD 13793  trintOLD 13794  dffr5 13831  elpotr 13847  poxp 13949  wfrlem5 13961  rb-bijust 14216  ref4w 14370  mnlmxl2 14611  vecval1b 14794  vecval3b 14795  svli2 14826  ordisoOLD 15374  compfipin0 15436  infmrlb 15765  infmrgelb 15766  txcnoprab 15911  isdmn3 16222  conss34 16419

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain