Theorem bibi12d 235

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32  453  bi2bian9  608  cleqh  2306  abbi  2320  cleqf  2374  cbvreuvw  2745  vtoclb  2832  vtoclbg  2836  ceqsexg  2905  elabgf  2919  reu6  2966  ru  3001  sbcbig  3049  sbcne12g  3115  sbcnestgf  3149  preq12bg  3822  nalset  4185  undifexmid  4248  exmidsssn  4257  exmidsssnc  4258  exmidundif  4261  opthg  4295  opelopabsb  4319  wetriext  4638  opeliunxp2  4831  resieq  4983  elimasng  5064  cbviota  5251  iota2df  5271  fnbrfvb  5637  fvelimab  5653  fmptco  5764  fsng  5771  fressnfv  5789  funfvima3  5836  isorel  5895  isocnv  5898  isocnv2  5899  isotr  5903  ovg  6103  caovcang  6126  caovordg  6132  caovord3d  6135  caovord  6136  uchoice  6241  opeliunxp2f  6342  dftpos4  6367  ecopovsym  6736  ecopovsymg  6739  xpf1o  6961  nneneq  6974  supmoti  7116  supsnti  7128  isotilem  7129  isoti  7130  ltanqg  7543  ltmnqg  7544  elinp  7617  prnmaxl  7631  prnminu  7632  ltasrg  7913  axpre-ltadd  8029  zextle  9494  zextlt  9495  xlesubadd  10035  rexfiuz  11385  climshft  11700  dvdsext  12251  ltoddhalfle  12289  halfleoddlt  12290  bezoutlemmo  12412  bezoutlemeu  12413  bezoutlemle  12414  bezoutlemsup  12415  dfgcd3  12416  dvdssq  12437  rpexp  12560  pcdvdsb  12728  isnsg  13623  nsgbi  13625  elnmz  13629  nmzbi  13630  nmznsg  13634  islidlm  14326  xmeteq0  14916  comet  15056  dedekindeulemuub  15174  dedekindeulemloc  15176  dedekindicclemuub  15183  dedekindicclemloc  15185  logltb  15431  bj-nalset  16000  bj-d0clsepcl  16030  bj-nn0sucALT  16083  ltlenmkv  16181