Theorem bibi12d 224

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	|- ( ph -> ( ps <-> ch ) )
imbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
bibi12d	|- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bibi1d 222	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 221	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 177	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.32  426  bi2bian9  540  cleqh  2137  abbi  2151  cleqf  2201  vtoclb  2611  vtoclbg  2614  ceqsexg  2672  elabgf  2685  reu6  2730  ru  2763  sbcbig  2809  sbcne12g  2868  sbcnestgf  2897  preq12bg  3544  nalset  3887  opthg  3975  opelopabsb  3997  wetriext  4301  opeliunxp2  4476  resieq  4622  elimasng  4693  cbviota  4872  iota2df  4891  fnbrfvb  5214  fvelimab  5229  fmptco  5330  fsng  5336  fressnfv  5350  funfvima3  5392  isorel  5448  isocnv  5451  isocnv2  5452  isotr  5456  ovg  5639  caovcang  5662  caovordg  5668  caovord3d  5671  caovord  5672  dftpos4  5878  ecopovsym  6202  ecopovsymg  6205  nneneq  6320  ltanqg  6498  ltmnqg  6499  elinp  6572  prnmaxl  6586  prnminu  6587  ltasrg  6855  axpre-ltadd  6960  zextle  8331  zextlt  8332  climshft  9825  bj-nalset  10015  bj-d0clsepcl  10049  bj-nn0sucALT  10103