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  2134  abbi  2148  cleqf  2198  vtoclb  2605  vtoclbg  2608  ceqsexg  2666  elabgf  2679  reu6  2724  ru  2757  sbcbig  2803  sbcne12g  2862  sbcnestgf  2891  preq12bg  3535  nalset  3878  opthg  3966  opelopabsb  3988  opeliunxp2  4419  resieq  4565  elimasng  4636  cbviota  4815  iota2df  4834  fnbrfvb  5157  fvelimab  5172  fmptco  5273  fsng  5279  fressnfv  5293  funfvima3  5335  isorel  5391  isocnv  5394  isocnv2  5395  isotr  5399  ovg  5581  caovcang  5604  caovordg  5610  caovord3d  5613  caovord  5614  dftpos4  5819  ecopovsym  6138  ecopovsymg  6141  ltanqg  6384  ltmnqg  6385  elinp  6457  prnmaxl  6471  prnminu  6472  ltasrg  6698  axpre-ltadd  6770  zextle  8107  zextlt  8108  bj-nalset  9350  bj-d0clsepcl  9384  bj-nn0sucALT  9438