Theorem bibi12d 233

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 231	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 230	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 186	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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:  pm5.32  441  bi2bian9  573  cleqh  2179  abbi  2193  cleqf  2243  vtoclb  2657  vtoclbg  2660  ceqsexg  2724  elabgf  2737  reu6  2782  ru  2815  sbcbig  2861  sbcne12g  2925  sbcnestgf  2954  preq12bg  3573  nalset  3916  opthg  4001  opelopabsb  4023  wetriext  4327  opeliunxp2  4504  resieq  4650  elimasng  4723  cbviota  4902  iota2df  4921  fnbrfvb  5246  fvelimab  5261  fmptco  5362  fsng  5368  fressnfv  5382  funfvima3  5424  isorel  5479  isocnv  5482  isocnv2  5483  isotr  5487  ovg  5670  caovcang  5693  caovordg  5699  caovord3d  5702  caovord  5703  dftpos4  5912  ecopovsym  6268  ecopovsymg  6271  xpf1o  6385  nneneq  6392  supmoti  6465  supsnti  6477  isotilem  6478  isoti  6479  ltanqg  6652  ltmnqg  6653  elinp  6726  prnmaxl  6740  prnminu  6741  ltasrg  7009  axpre-ltadd  7114  zextle  8519  zextlt  8520  rexfiuz  10013  climshft  10281  dvdsext  10400  ltoddhalfle  10437  halfleoddlt  10438  bezoutlemmo  10539  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dvdssq  10564  rpexp  10676  bj-nalset  10844  bj-d0clsepcl  10878  bj-nn0sucALT  10931