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  440  bi2bian9  572  cleqh  2178  abbi  2192  cleqf  2242  vtoclb  2656  vtoclbg  2659  ceqsexg  2723  elabgf  2736  reu6  2781  ru  2814  sbcbig  2860  sbcne12g  2924  sbcnestgf  2953  preq12bg  3565  nalset  3908  opthg  3993  opelopabsb  4015  wetriext  4319  opeliunxp2  4494  resieq  4640  elimasng  4713  cbviota  4892  iota2df  4911  fnbrfvb  5235  fvelimab  5250  fmptco  5351  fsng  5357  fressnfv  5371  funfvima3  5413  isorel  5468  isocnv  5471  isocnv2  5472  isotr  5476  ovg  5659  caovcang  5682  caovordg  5688  caovord3d  5691  caovord  5692  dftpos4  5901  ecopovsym  6225  ecopovsymg  6228  nneneq  6343  supmoti  6406  supsnti  6418  isotilem  6419  isoti  6420  ltanqg  6590  ltmnqg  6591  elinp  6664  prnmaxl  6678  prnminu  6679  ltasrg  6947  axpre-ltadd  7052  zextle  8438  zextlt  8439  rexfiuz  9875  climshft  10143  dvdsext  10255  ltoddhalfle  10293  halfleoddlt  10294  bezoutlemmo  10395  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dvdssq  10420  rpexp  10532  bj-nalset  10686  bj-d0clsepcl  10720  bj-nn0sucALT  10773