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-mp 5  ax-1 6  ax-2 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  449  bi2bian9  598  cleqh  2265  abbi  2279  cleqf  2332  cbvreuvw  2697  vtoclb  2782  vtoclbg  2786  ceqsexg  2853  elabgf  2867  reu6  2914  ru  2949  sbcbig  2996  sbcne12g  3062  sbcnestgf  3095  preq12bg  3752  nalset  4111  undifexmid  4171  exmidsssn  4180  exmidsssnc  4181  exmidundif  4184  opthg  4215  opelopabsb  4237  wetriext  4553  opeliunxp2  4743  resieq  4893  elimasng  4971  cbviota  5157  iota2df  5176  fnbrfvb  5526  fvelimab  5541  fmptco  5650  fsng  5657  fressnfv  5671  funfvima3  5717  isorel  5775  isocnv  5778  isocnv2  5779  isotr  5783  ovg  5976  caovcang  5999  caovordg  6005  caovord3d  6008  caovord  6009  opeliunxp2f  6202  dftpos4  6227  ecopovsym  6593  ecopovsymg  6596  xpf1o  6806  nneneq  6819  supmoti  6954  supsnti  6966  isotilem  6967  isoti  6968  ltanqg  7337  ltmnqg  7338  elinp  7411  prnmaxl  7425  prnminu  7426  ltasrg  7707  axpre-ltadd  7823  zextle  9278  zextlt  9279  xlesubadd  9815  rexfiuz  10927  climshft  11241  dvdsext  11789  ltoddhalfle  11826  halfleoddlt  11827  bezoutlemmo  11935  bezoutlemeu  11936  bezoutlemle  11937  bezoutlemsup  11938  dfgcd3  11939  dvdssq  11960  rpexp  12081  pcdvdsb  12247  xmeteq0  12959  comet  13099  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindicclemuub  13204  dedekindicclemloc  13206  logltb  13395  bj-nalset  13737  bj-d0clsepcl  13767  bj-nn0sucALT  13820