Theorem bibi12d 234

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32  442  bi2bian9  576  cleqh  2194  abbi  2208  cleqf  2259  vtoclb  2690  vtoclbg  2694  ceqsexg  2759  elabgf  2772  reu6  2818  ru  2853  sbcbig  2899  sbcne12g  2963  sbcnestgf  2993  preq12bg  3639  nalset  3990  undifexmid  4049  exmidsssn  4055  exmidundif  4058  opthg  4089  opelopabsb  4111  wetriext  4420  opeliunxp2  4607  resieq  4755  elimasng  4833  cbviota  5019  iota2df  5038  fnbrfvb  5380  fvelimab  5395  fmptco  5503  fsng  5509  fressnfv  5523  funfvima3  5567  isorel  5625  isocnv  5628  isocnv2  5629  isotr  5633  ovg  5821  caovcang  5844  caovordg  5850  caovord3d  5853  caovord  5854  opeliunxp2f  6041  dftpos4  6066  ecopovsym  6428  ecopovsymg  6431  xpf1o  6640  nneneq  6653  supmoti  6768  supsnti  6780  isotilem  6781  isoti  6782  ltanqg  7056  ltmnqg  7057  elinp  7130  prnmaxl  7144  prnminu  7145  ltasrg  7413  axpre-ltadd  7518  zextle  8936  zextlt  8937  xlesubadd  9449  rexfiuz  10537  climshft  10847  dvdsext  11283  ltoddhalfle  11320  halfleoddlt  11321  bezoutlemmo  11422  bezoutlemeu  11423  bezoutlemle  11424  bezoutlemsup  11425  dfgcd3  11426  dvdssq  11447  rpexp  11559  xmeteq0  12145  comet  12285  bj-nalset  12494  bj-d0clsepcl  12528  bj-nn0sucALT  12581