Theorem bibi12d 321

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 319	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 318	. 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  865  xorbi12d  1359  sb8eu  2295  cleqh  2538  abbi  2551  cleqf  2601  vtoclb  3024  vtoclbg  3028  ceqsexg  3088  elabgf  3101  reu6  3145  ru  3182  sbcbig  3230  unineq  3597  sbcnestgf  3688  preq12bg  4048  prel12g  4049  axrep1  4401  axrep4  4404  nalset  4426  opthg  4564  opelopabsb  4597  isso2i  4669  opeliunxp2  4974  resieq  5117  elimasng  5192  cbviota  5383  iota2df  5402  fnbrfvb  5729  fvelimab  5744  fvopab5  5792  fmptco  5873  fsng  5879  fressnfv  5893  isorel  6014  isocnv  6018  isocnv3  6020  isotr  6024  ovg  6228  caovcang  6263  caovordg  6269  caovord3d  6272  caovord  6273  orduninsuc  6453  brtpos  6753  dftpos4  6763  omopth  7093  ecopovsym  7198  xpf1o  7469  nneneq  7490  r1pwOLD  8049  karden  8098  infxpenlem  8176  aceq0  8284  cflim2  8428  zfac  8625  ttukeylem1  8674  axextnd  8751  axrepndlem1  8752  axrepndlem2  8753  axrepnd  8754  axacndlem5  8774  zfcndrep  8777  zfcndac  8782  winalim  8858  gruina  8981  ltrnq  9144  ltsosr  9257  ltasr  9263  axpre-lttri  9328  axpre-ltadd  9330  nn0sub  10626  zextle  10711  zextlt  10712  xlesubadd  11222  sqeqor  11976  nn0opth2  12046  rexfiuz  12831  climshft  13050  rpnnen2lem10  13502  dvdsext  13580  sadcadd  13650  dvdssq  13740  isprm2lem  13766  rpexp  13802  pcdvdsb  13931  imasleval  14475  isacs2  14587  acsfiel  14588  funcres2b  14803  pospropd  15300  isnsg  15703  nsgbi  15705  elnmz  15713  nmzbi  15714  oddvdsnn0  16040  odeq  16046  odmulg  16050  isslw  16100  slwispgp  16103  gsumval3OLD  16375  gsumval3lem2  16377  gsumcom2  16457  abveq0  16891  cnt0  18909  kqfvima  19262  kqt0lem  19268  isr0  19269  r0cld  19270  regr1lem2  19272  nrmr0reg  19281  isfildlem  19389  cnextfvval  19596  xmeteq0  19872  imasf1oxmet  19909  comet  20047  dscmet  20124  nrmmetd  20126  tngngp  20199  mbfsup  21101  mbfinf  21102  degltlem1  21502  logltb  22007  cxple2  22101  rlimcnp  22318  rlimcnp2  22319  isppw2  22412  sqf11  22436  f1otrgitv  23051  eupath2lem3  23535  nmlno0i  24129  nmlno0  24130  blocn  24142  ubth  24209  hvsubeq0  24405  hvaddcan  24407  hvsubadd  24414  normsub0  24473  hlim2  24529  pjoc1  24772  pjoc2  24777  chne0  24832  chsscon3  24838  chlejb1  24850  chnle  24852  h1de2ci  24894  elspansn  24904  elspansn2  24905  cmbr3  24946  cmcm  24952  cmcm3  24953  pjch1  25008  pjch  25032  pj11  25052  pjnel  25064  eigorth  25177  elnlfn  25267  nmlnop0  25337  lnopeq  25348  lnopcon  25374  lnfncon  25395  pjdifnormi  25506  chrelat2  25709  cvexch  25713  mdsym  25751  fmptcof2  25914  fcnvgreu  25926  signswch  26892  cvmlift2lem12  27133  cvmlift2lem13  27134  abs2sqle  27254  abs2sqlt  27255  dfpo2  27494  axextdist  27542  brimageg  27887  brdomaing  27895  brrangeg  27896  elhf2  28142  onsuct0  28217  nn0prpwlem  28442  nn0prpw  28443  prdsbnd2  28619  isdrngo1  28687  sbcalf  28845  sbcexf  28846  zindbi  29212  divalgmodcl  29261  wepwsolem  29319  aomclem8  29339  2sbc6g  29594  2sbc5g  29595  bj-cleqh  32055  bj-abbi  32058  bj-axrep1  32069  bj-axrep4  32072  bj-nalset  32075  bj-sbceqgALT  32142  lsatcmp  32370  llnexchb2  33235  lautset  33448  lautle  33450