Theorem bibi12d 319

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-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 317	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 316	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 253	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  bi2bian9  873  xorbi12d  1379  sb8eu  2319  cleqh  2569  cleqhOLD  2570  abbiOLD  2586  cleqfOLD  2644  vtoclb  3161  vtoclbg  3165  ceqsexg  3228  elabgf  3241  reu6  3285  ru  3323  sbcbig  3369  unineq  3745  sbcnestgf  3834  preq12bg  4195  prel12g  4196  axrep1  4551  axrep4  4554  nalset  4574  opthg  4712  opelopabsb  4746  isso2i  4821  opeliunxp2  5130  resieq  5272  elimasng  5351  cbviota  5539  iota2df  5558  fnbrfvb  5888  fvelimab  5904  fvopab5  5955  fmptco  6040  fsng  6046  fressnfv  6061  isorel  6197  isocnv  6201  isocnv3  6203  isotr  6207  ovg  6414  caovcang  6449  caovordg  6455  caovord3d  6458  caovord  6459  orduninsuc  6651  brtpos  6956  dftpos4  6966  omopth  7299  ecopovsym  7405  xpf1o  7672  nneneq  7693  r1pwALT  8255  karden  8304  infxpenlem  8382  aceq0  8490  cflim2  8634  zfac  8831  ttukeylem1  8880  axextnd  8957  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axacndlem5  8978  zfcndrep  8981  zfcndac  8986  winalim  9062  gruina  9185  ltrnq  9346  ltsosr  9460  ltasr  9466  axpre-lttri  9531  axpre-ltadd  9533  nn0sub  10842  zextle  10932  zextlt  10933  xlesubadd  11458  sqeqor  12264  nn0opth2  12334  rexfiuz  13262  climshft  13481  rpnnen2lem10  14041  dvdsext  14121  sadcadd  14192  dvdssq  14282  isprm2lem  14308  rpexp  14345  pcdvdsb  14476  imasleval  15030  isacs2  15142  acsfiel  15143  funcres2b  15385  pospropd  15963  isnsg  16429  nsgbi  16431  elnmz  16439  nmzbi  16440  oddvdsnn0  16767  odeq  16773  odmulg  16777  isslw  16827  slwispgp  16830  gsumval3OLD  17107  gsumval3lem2  17109  gsumcom2  17199  abveq0  17670  cnt0  20014  kqfvima  20397  kqt0lem  20403  isr0  20404  r0cld  20405  regr1lem2  20407  nrmr0reg  20416  isfildlem  20524  cnextfvval  20731  xmeteq0  21007  imasf1oxmet  21044  comet  21182  dscmet  21259  nrmmetd  21261  tngngp  21334  mbfsup  22237  mbfinf  22238  degltlem1  22638  logltb  23153  cxple2  23246  rlimcnp  23493  rlimcnp2  23494  isppw2  23587  sqf11  23611  f1otrgitv  24375  isrgrac  25136  eupath2lem3  25181  nmlno0i  25907  nmlno0  25908  blocn  25920  ubth  25987  hvsubeq0  26183  hvaddcan  26185  hvsubadd  26192  normsub0  26251  hlim2  26307  pjoc1  26550  pjoc2  26555  chne0  26610  chsscon3  26616  chlejb1  26628  chnle  26630  h1de2ci  26672  elspansn  26682  elspansn2  26683  cmbr3  26724  cmcm  26730  cmcm3  26731  pjch1  26786  pjch  26810  pj11  26830  pjnel  26842  eigorth  26955  elnlfn  27045  nmlnop0  27115  lnopeq  27126  lnopcon  27152  lnfncon  27173  pjdifnormi  27284  chrelat2  27487  cvexch  27491  mdsym  27529  fmptcof2  27724  signswch  28782  cvmlift2lem12  29023  cvmlift2lem13  29024  abs2sqle  29310  abs2sqlt  29311  dfpo2  29425  axextdist  29472  brimageg  29805  brdomaing  29813  brrangeg  29814  elhf2  30060  onsuct0  30134  nn0prpwlem  30380  nn0prpw  30381  prdsbnd2  30531  isdrngo1  30599  zindbi  31121  divalgmodcl  31168  wepwsolem  31226  aomclem8  31246  2sbc6g  31563  2sbc5g  31564  fourierdlem31  32159  fourierdlem42  32170  fourierdlem54  32182  bj-cleqh  34759  bj-abbi  34762  bj-axrep1  34775  bj-axrep4  34778  bj-nalset  34781  bj-sbceqgALT  34870  bj-ru0  34901  lsatcmp  35125  llnexchb2  35990  lautset  36203  lautle  36205