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  1374  sb8eu  2314  cleqh  2582  cleqhOLD  2583  abbiOLD  2599  cleqfOLD  2657  vtoclb  3168  vtoclbg  3172  ceqsexg  3235  elabgf  3248  reu6  3292  ru  3330  sbcbig  3378  unineq  3748  sbcnestgf  3839  preq12bg  4205  prel12g  4206  axrep1  4559  axrep4  4562  nalset  4584  opthg  4722  opelopabsb  4757  isso2i  4832  opeliunxp2  5141  resieq  5284  elimasng  5363  cbviota  5556  iota2df  5575  fnbrfvb  5908  fvelimab  5924  fvopab5  5974  fmptco  6055  fsng  6061  fressnfv  6076  isorel  6211  isocnv  6215  isocnv3  6217  isotr  6221  ovg  6426  caovcang  6461  caovordg  6467  caovord3d  6470  caovord  6471  orduninsuc  6663  brtpos  6965  dftpos4  6975  omopth  7308  ecopovsym  7414  xpf1o  7680  nneneq  7701  r1pwOLD  8265  karden  8314  infxpenlem  8392  aceq0  8500  cflim2  8644  zfac  8841  ttukeylem1  8890  axextnd  8967  axrepndlem1  8968  axrepndlem2  8969  axrepnd  8970  axacndlem5  8990  zfcndrep  8993  zfcndac  8998  winalim  9074  gruina  9197  ltrnq  9358  ltsosr  9472  ltasr  9478  axpre-lttri  9543  axpre-ltadd  9545  nn0sub  10847  zextle  10935  zextlt  10936  xlesubadd  11456  sqeqor  12251  nn0opth2  12321  rexfiuz  13146  climshft  13365  rpnnen2lem10  13821  dvdsext  13899  sadcadd  13970  dvdssq  14060  isprm2lem  14086  rpexp  14123  pcdvdsb  14254  imasleval  14799  isacs2  14911  acsfiel  14912  funcres2b  15127  pospropd  15624  isnsg  16044  nsgbi  16046  elnmz  16054  nmzbi  16055  oddvdsnn0  16383  odeq  16389  odmulg  16393  isslw  16443  slwispgp  16446  gsumval3OLD  16723  gsumval3lem2  16725  gsumcom2  16818  abveq0  17287  cnt0  19653  kqfvima  20058  kqt0lem  20064  isr0  20065  r0cld  20066  regr1lem2  20068  nrmr0reg  20077  isfildlem  20185  cnextfvval  20392  xmeteq0  20668  imasf1oxmet  20705  comet  20843  dscmet  20920  nrmmetd  20922  tngngp  20995  mbfsup  21898  mbfinf  21899  degltlem1  22299  logltb  22809  cxple2  22903  rlimcnp  23120  rlimcnp2  23121  isppw2  23214  sqf11  23238  f1otrgitv  23946  isrgrac  24707  eupath2lem3  24752  nmlno0i  25482  nmlno0  25483  blocn  25495  ubth  25562  hvsubeq0  25758  hvaddcan  25760  hvsubadd  25767  normsub0  25826  hlim2  25882  pjoc1  26125  pjoc2  26130  chne0  26185  chsscon3  26191  chlejb1  26203  chnle  26205  h1de2ci  26247  elspansn  26257  elspansn2  26258  cmbr3  26299  cmcm  26305  cmcm3  26306  pjch1  26361  pjch  26385  pj11  26405  pjnel  26417  eigorth  26530  elnlfn  26620  nmlnop0  26690  lnopeq  26701  lnopcon  26727  lnfncon  26748  pjdifnormi  26859  chrelat2  27062  cvexch  27066  mdsym  27104  fmptcof2  27271  fcnvgreu  27283  signswch  28269  cvmlift2lem12  28510  cvmlift2lem13  28511  abs2sqle  28797  abs2sqlt  28798  dfpo2  29037  axextdist  29085  brimageg  29430  brdomaing  29438  brrangeg  29439  elhf2  29685  onsuct0  29759  nn0prpwlem  29993  nn0prpw  29994  prdsbnd2  30121  isdrngo1  30189  sbcalf  30347  sbcexf  30348  zindbi  30713  divalgmodcl  30760  wepwsolem  30818  aomclem8  30838  2sbc6g  31127  2sbc5g  31128  fourierdlem31  31665  fourierdlem42  31676  fourierdlem54  31688  bj-cleqh  33656  bj-abbi  33659  bj-axrep1  33672  bj-axrep4  33675  bj-nalset  33678  bj-sbceqgALT  33767  bj-ru0  33798  lsatcmp  34017  llnexchb2  34882  lautset  35095  lautle  35097