Theorem bibi12d 327

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

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

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 190

This theorem is referenced by:  bi2bian9  891  xorbi12d  1432  sb8eu  2343  cleqh  2563  vtoclb  3116  vtoclbg  3120  ceqsexg  3182  elabgf  3195  reu6  3239  ru  3278  sbcbig  3324  unineq  3705  sbcnestgf  3796  preq12bg  4168  prel12g  4169  axrep1  4530  axrep4  4533  nalset  4554  opthg  4691  opelopabsb  4725  isso2i  4806  opeliunxp2  4992  resieq  5134  elimasng  5213  cbviota  5570  iota2df  5589  fnbrfvb  5928  fvelimab  5944  fvopab5  5997  fmptco  6080  fsng  6087  fsn2g  6088  fressnfv  6102  fnpr2g  6149  isorel  6242  isocnv  6246  isocnv3  6248  isotr  6252  ovg  6462  caovcang  6497  caovordg  6503  caovord3d  6506  caovord  6507  orduninsuc  6697  opeliunxp2f  6983  brtpos  7008  dftpos4  7018  omopth  7385  ecopovsym  7491  xpf1o  7760  nneneq  7781  r1pwALT  8343  karden  8392  infxpenlem  8470  aceq0  8575  cflim2  8719  zfac  8916  ttukeylem1  8965  axextnd  9042  axrepndlem1  9043  axrepndlem2  9044  axrepnd  9045  axacndlem5  9062  zfcndrep  9065  zfcndac  9070  winalim  9146  gruina  9269  ltrnq  9430  ltsosr  9544  ltasr  9550  axpre-lttri  9615  axpre-ltadd  9617  nn0sub  10949  zextle  11038  zextlt  11039  xlesubadd  11578  sqeqor  12420  nn0opth2  12490  rexfiuz  13459  climshft  13689  rpnnen2lem10  14325  dvdsext  14405  sadcadd  14481  dvdssq  14577  isprm2lem  14680  rpexp  14721  pcdvdsb  14867  imasleval  15496  isacs2  15608  acsfiel  15609  funcres2b  15851  pospropd  16429  isnsg  16895  nsgbi  16897  elnmz  16905  nmzbi  16906  oddvdsnn0  17242  odeq  17248  odmulg  17256  isslw  17309  slwispgp  17312  gsumval3lem2  17589  gsumcom2  17656  abveq0  18103  cnt0  20411  kqfvima  20794  kqt0lem  20800  isr0  20801  r0cld  20802  regr1lem2  20804  nrmr0reg  20813  isfildlem  20921  cnextfvval  21129  xmeteq0  21402  imasf1oxmet  21439  comet  21577  dscmet  21636  nrmmetd  21638  tngngp  21711  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  degltlem1  23070  logltb  23598  cxple2  23691  rlimcnp  23940  rlimcnp2  23941  isppw2  24091  sqf11  24115  f1otrgitv  24949  isrgrac  25711  eupath2lem3  25756  nmlno0i  26484  nmlno0  26485  blocn  26497  ubth  26564  hvsubeq0  26770  hvaddcan  26772  hvsubadd  26779  normsub0  26838  hlim2  26894  pjoc1  27136  pjoc2  27141  chne0  27196  chsscon3  27202  chlejb1  27214  chnle  27216  h1de2ci  27258  elspansn  27268  elspansn2  27269  cmbr3  27310  cmcm  27316  cmcm3  27317  pjch1  27372  pjch  27396  pj11  27416  pjnel  27428  eigorth  27540  elnlfn  27630  nmlnop0  27700  lnopeq  27711  lnopcon  27737  lnfncon  27758  pjdifnormi  27869  chrelat2  28072  cvexch  28076  mdsym  28114  fmptcof2  28308  signswch  29499  cvmlift2lem12  30086  cvmlift2lem13  30087  abs2sqle  30373  abs2sqlt  30374  dfpo2  30444  br1steqg  30465  br2ndeqg  30466  axextdist  30495  brimageg  30743  brdomaing  30751  brrangeg  30752  elhf2  30991  nn0prpwlem  31027  nn0prpw  31028  onsuct0  31150  bj-abbi  31435  bj-axrep1  31448  bj-axrep4  31451  bj-nalset  31454  bj-sbceqgALT  31549  bj-ru0  31582  prdsbnd2  32172  isdrngo1  32240  lsatcmp  32614  llnexchb2  33479  lautset  33692  lautle  33694  zindbi  35839  divalgmodcl  35887  wepwsolem  35945  aomclem8  35964  2sbc6g  36810  2sbc5g  36811  wessf1ornlem  37497  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem54  38062  nbuhgr2vtx1edgb  39470  dfconngr1  39929