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  450  bi2bian9  603  cleqh  2270  abbi  2284  cleqf  2337  cbvreuvw  2702  vtoclb  2787  vtoclbg  2791  ceqsexg  2858  elabgf  2872  reu6  2919  ru  2954  sbcbig  3001  sbcne12g  3067  sbcnestgf  3100  preq12bg  3758  nalset  4117  undifexmid  4177  exmidsssn  4186  exmidsssnc  4187  exmidundif  4190  opthg  4221  opelopabsb  4243  wetriext  4559  opeliunxp2  4749  resieq  4899  elimasng  4977  cbviota  5163  iota2df  5182  fnbrfvb  5535  fvelimab  5550  fmptco  5660  fsng  5667  fressnfv  5681  funfvima3  5727  isorel  5785  isocnv  5788  isocnv2  5789  isotr  5793  ovg  5989  caovcang  6012  caovordg  6018  caovord3d  6021  caovord  6022  opeliunxp2f  6215  dftpos4  6240  ecopovsym  6606  ecopovsymg  6609  xpf1o  6819  nneneq  6832  supmoti  6967  supsnti  6979  isotilem  6980  isoti  6981  ltanqg  7351  ltmnqg  7352  elinp  7425  prnmaxl  7439  prnminu  7440  ltasrg  7721  axpre-ltadd  7837  zextle  9292  zextlt  9293  xlesubadd  9829  rexfiuz  10942  climshft  11256  dvdsext  11804  ltoddhalfle  11841  halfleoddlt  11842  bezoutlemmo  11950  bezoutlemeu  11951  bezoutlemle  11952  bezoutlemsup  11953  dfgcd3  11954  dvdssq  11975  rpexp  12096  pcdvdsb  12262  xmeteq0  13114  comet  13254  dedekindeulemuub  13350  dedekindeulemloc  13352  dedekindicclemuub  13359  dedekindicclemloc  13361  logltb  13550  bj-nalset  13892  bj-d0clsepcl  13922  bj-nn0sucALT  13975