Theorem bibi12d 322

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

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

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 188

This theorem is referenced by:  bi2bian9  883  xorbi12d  1417  sb8eu  2297  cleqh  2535  cleqhOLD  2536  abbiOLD  2552  cleqfOLD  2610  vtoclb  3133  vtoclbg  3137  ceqsexg  3200  elabgf  3213  reu6  3257  ru  3295  sbcbig  3341  unineq  3720  sbcnestgf  3809  preq12bg  4173  prel12g  4174  axrep1  4530  axrep4  4533  nalset  4553  opthg  4688  opelopabsb  4722  isso2i  4798  opeliunxp2  4984  resieq  5126  elimasng  5205  cbviota  5561  iota2df  5580  fnbrfvb  5912  fvelimab  5928  fvopab5  5980  fmptco  6062  fsng  6069  fsn2g  6070  fressnfv  6084  fnpr2g  6130  isorel  6223  isocnv  6227  isocnv3  6229  isotr  6233  ovg  6440  caovcang  6475  caovordg  6481  caovord3d  6484  caovord  6485  orduninsuc  6675  brtpos  6981  dftpos4  6991  omopth  7358  ecopovsym  7464  xpf1o  7731  nneneq  7752  r1pwALT  8307  karden  8356  infxpenlem  8434  aceq0  8538  cflim2  8682  zfac  8879  ttukeylem1  8928  axextnd  9005  axrepndlem1  9006  axrepndlem2  9007  axrepnd  9008  axacndlem5  9025  zfcndrep  9028  zfcndac  9033  winalim  9109  gruina  9232  ltrnq  9393  ltsosr  9507  ltasr  9513  axpre-lttri  9578  axpre-ltadd  9580  nn0sub  10909  zextle  10998  zextlt  10999  xlesubadd  11538  sqeqor  12374  nn0opth2  12444  rexfiuz  13378  climshft  13607  rpnnen2lem10  14243  dvdsext  14323  sadcadd  14395  dvdssq  14488  isprm2lem  14591  rpexp  14632  pcdvdsb  14770  imasleval  15391  isacs2  15503  acsfiel  15504  funcres2b  15746  pospropd  16324  isnsg  16790  nsgbi  16792  elnmz  16800  nmzbi  16801  oddvdsnn0  17128  odeq  17134  odmulg  17138  isslw  17188  slwispgp  17191  gsumval3lem2  17468  gsumcom2  17535  abveq0  17982  cnt0  20286  kqfvima  20669  kqt0lem  20675  isr0  20676  r0cld  20677  regr1lem2  20679  nrmr0reg  20688  isfildlem  20796  cnextfvval  21004  xmeteq0  21277  imasf1oxmet  21314  comet  21452  dscmet  21511  nrmmetd  21513  tngngp  21586  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  degltlem1  22895  logltb  23411  cxple2  23504  rlimcnp  23753  rlimcnp2  23754  isppw2  23902  sqf11  23926  f1otrgitv  24743  isrgrac  25504  eupath2lem3  25549  nmlno0i  26277  nmlno0  26278  blocn  26290  ubth  26357  hvsubeq0  26553  hvaddcan  26555  hvsubadd  26562  normsub0  26621  hlim2  26677  pjoc1  26919  pjoc2  26924  chne0  26979  chsscon3  26985  chlejb1  26997  chnle  26999  h1de2ci  27041  elspansn  27051  elspansn2  27052  cmbr3  27093  cmcm  27099  cmcm3  27100  pjch1  27155  pjch  27179  pj11  27199  pjnel  27211  eigorth  27323  elnlfn  27413  nmlnop0  27483  lnopeq  27494  lnopcon  27520  lnfncon  27541  pjdifnormi  27652  chrelat2  27855  cvexch  27859  mdsym  27897  fmptcof2  28096  signswch  29235  cvmlift2lem12  29822  cvmlift2lem13  29823  abs2sqle  30109  abs2sqlt  30110  dfpo2  30179  br1steqg  30200  br2ndeqg  30201  axextdist  30230  brimageg  30476  brdomaing  30484  brrangeg  30485  elhf2  30724  nn0prpwlem  30760  nn0prpw  30761  onsuct0  30883  bj-cleqh  31135  bj-abbi  31138  bj-axrep1  31151  bj-axrep4  31154  bj-nalset  31157  bj-sbceqgALT  31251  bj-ru0  31283  prdsbnd2  31831  isdrngo1  31899  lsatcmp  32278  llnexchb2  33143  lautset  33356  lautle  33358  zindbi  35504  divalgmodcl  35552  wepwsolem  35610  aomclem8  35629  2sbc6g  36407  2sbc5g  36408  wessf1ornlem  37086  fourierdlem31  37573  fourierdlem42  37584  fourierdlem54  37596