Theorem bibi12d 321

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 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  873  xorbi12d  1376  sb8eu  2302  cleqh  2556  cleqhOLD  2557  abbiOLD  2573  cleqfOLD  2631  vtoclb  3148  vtoclbg  3152  ceqsexg  3215  elabgf  3228  reu6  3272  ru  3310  sbcbig  3358  unineq  3731  sbcnestgf  3822  preq12bg  4191  prel12g  4192  axrep1  4546  axrep4  4549  nalset  4571  opthg  4709  opelopabsb  4744  isso2i  4819  opeliunxp2  5128  resieq  5271  elimasng  5350  cbviota  5543  iota2df  5562  fnbrfvb  5895  fvelimab  5911  fvopab5  5961  fmptco  6046  fsng  6052  fressnfv  6067  isorel  6204  isocnv  6208  isocnv3  6210  isotr  6214  ovg  6423  caovcang  6458  caovordg  6464  caovord3d  6467  caovord  6468  orduninsuc  6660  brtpos  6963  dftpos4  6973  omopth  7306  ecopovsym  7412  xpf1o  7678  nneneq  7699  r1pwOLD  8264  karden  8313  infxpenlem  8391  aceq0  8499  cflim2  8643  zfac  8840  ttukeylem1  8889  axextnd  8966  axrepndlem1  8967  axrepndlem2  8968  axrepnd  8969  axacndlem5  8989  zfcndrep  8992  zfcndac  8997  winalim  9073  gruina  9196  ltrnq  9357  ltsosr  9471  ltasr  9477  axpre-lttri  9542  axpre-ltadd  9544  nn0sub  10849  zextle  10939  zextlt  10940  xlesubadd  11461  sqeqor  12258  nn0opth2  12328  rexfiuz  13156  climshft  13375  rpnnen2lem10  13831  dvdsext  13911  sadcadd  13982  dvdssq  14072  isprm2lem  14098  rpexp  14135  pcdvdsb  14266  imasleval  14812  isacs2  14924  acsfiel  14925  funcres2b  15137  pospropd  15635  isnsg  16101  nsgbi  16103  elnmz  16111  nmzbi  16112  oddvdsnn0  16439  odeq  16445  odmulg  16449  isslw  16499  slwispgp  16502  gsumval3OLD  16779  gsumval3lem2  16781  gsumcom2  16874  abveq0  17346  cnt0  19717  kqfvima  20101  kqt0lem  20107  isr0  20108  r0cld  20109  regr1lem2  20111  nrmr0reg  20120  isfildlem  20228  cnextfvval  20435  xmeteq0  20711  imasf1oxmet  20748  comet  20886  dscmet  20963  nrmmetd  20965  tngngp  21038  mbfsup  21941  mbfinf  21942  degltlem1  22342  logltb  22853  cxple2  22947  rlimcnp  23164  rlimcnp2  23165  isppw2  23258  sqf11  23282  f1otrgitv  24042  isrgrac  24803  eupath2lem3  24848  nmlno0i  25578  nmlno0  25579  blocn  25591  ubth  25658  hvsubeq0  25854  hvaddcan  25856  hvsubadd  25863  normsub0  25922  hlim2  25978  pjoc1  26221  pjoc2  26226  chne0  26281  chsscon3  26287  chlejb1  26299  chnle  26301  h1de2ci  26343  elspansn  26353  elspansn2  26354  cmbr3  26395  cmcm  26401  cmcm3  26402  pjch1  26457  pjch  26481  pj11  26501  pjnel  26513  eigorth  26626  elnlfn  26716  nmlnop0  26786  lnopeq  26797  lnopcon  26823  lnfncon  26844  pjdifnormi  26955  chrelat2  27158  cvexch  27162  mdsym  27200  fmptcof2  27371  signswch  28388  cvmlift2lem12  28629  cvmlift2lem13  28630  abs2sqle  28916  abs2sqlt  28917  dfpo2  29156  axextdist  29204  brimageg  29549  brdomaing  29557  brrangeg  29558  elhf2  29804  onsuct0  29878  nn0prpwlem  30112  nn0prpw  30113  prdsbnd2  30263  isdrngo1  30331  zindbi  30854  divalgmodcl  30901  wepwsolem  30959  aomclem8  30979  2sbc6g  31273  2sbc5g  31274  fourierdlem31  31809  fourierdlem42  31820  fourierdlem54  31832  bj-cleqh  34091  bj-abbi  34094  bj-axrep1  34107  bj-axrep4  34110  bj-nalset  34113  bj-sbceqgALT  34202  bj-ru0  34233  lsatcmp  34451  llnexchb2  35316  lautset  35529  lautle  35531