Theorem bibi12d 345

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
imbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
imbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
bibi12d	⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bibi1d 343	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 342	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bi2bian9  640  xorbi12d  1521  norass  1533  ru0  2124  sbbib  2361  sb8eulem  2595  abbib  2808  cleqh  2868  cleqf  2931  vtoclbg  3556  vtoclb  3567  ceqsexg  3652  elabgf  3674  elabgOLD  3677  reu6  3734  ruOLD  3789  sbcbig  3845  unineq  4293  sbcnestgfw  4426  sbcnestgf  4431  preq12bg  4857  axrep1  5285  axrep4OLD  5291  nalset  5318  opthg  5487  opelopabsb  5539  isso2i  5632  opeliunxp2  5851  resieq  6010  elimasngOLD  6110  dfpo2  6317  cbviotaw  6522  cbviota  6524  iota2df  6549  fnbrfvb  6959  fvelimab  6980  fvopab5  7048  fmptco  7148  fsng  7156  fressnfv  7179  fnpr2g  7229  isorel  7345  isocnv  7349  isocnv3  7351  isotr  7355  eqfunresadj  7379  ovg  7597  caovcang  7633  caovordg  7639  caovord3d  7642  caovord  7643  orduninsuc  7863  xpord2pred  8168  xpord3pred  8175  opeliunxp2f  8233  brtpos  8258  dftpos4  8268  omopth  8698  ecopovsym  8857  xpf1o  9177  nneneq  9243  nneneqOLD  9255  ttrclselem2  9763  r1pwALT  9883  karden  9932  infxpenlem  10050  aceq0  10155  cflim2  10300  zfac  10497  ttukeylem1  10546  axextnd  10628  axrepndlem1  10629  axrepndlem2  10630  axrepnd  10631  axacndlem5  10648  zfcndrep  10651  zfcndac  10656  winalim  10732  gruina  10855  ltrnq  11016  ltsosr  11131  ltasr  11137  axpre-lttri  11202  axpre-ltadd  11204  nn0sub  12573  zextle  12688  zextlt  12689  xlesubadd  13301  sqeqor  14251  nn0opth2  14307  rexfiuz  15382  climshft  15608  rpnnen2lem10  16255  dvdsext  16354  ltoddhalfle  16394  halfleoddlt  16395  sumodd  16421  sadcadd  16491  dvdssq  16600  rpexp  16755  pcdvdsb  16902  imasleval  17587  isacs2  17697  acsfiel  17698  funcres2b  17947  pospropd  18384  isnsg  19185  nsgbi  19187  elnmz  19193  nmzbi  19194  oddvdsnn0  19576  odeq  19582  odmulg  19588  isslw  19640  slwispgp  19643  gsumval3lem2  19938  gsumcom2  20007  abveq0  20835  cnt0  23369  kqfvima  23753  kqt0lem  23759  isr0  23760  r0cld  23761  regr1lem2  23763  nrmr0reg  23772  isfildlem  23880  cnextfvval  24088  xmeteq0  24363  imasf1oxmet  24400  comet  24541  dscmet  24600  nrmmetd  24602  tngngp  24690  tngngp3  24692  mbfsup  25712  mbfinf  25713  degltlem1  26125  logltb  26656  cxple2  26753  rlimcnp  27022  rlimcnp2  27023  isppw2  27172  sqf11  27196  slerec  27878  tgjustc1  28497  tgjustc2  28498  f1otrgitv  28892  nbuhgr2vtx1edgb  29383  dfconngr1  30216  eupth2lem3lem6  30261  nmlno0i  30822  nmlno0  30823  blocn  30835  ubth  30901  hvsubeq0  31096  hvaddcan  31098  hvsubadd  31105  normsub0  31164  hlim2  31220  pjoc1  31462  pjoc2  31467  chne0  31522  chsscon3  31528  chlejb1  31540  chnle  31542  h1de2ci  31584  elspansn  31594  elspansn2  31595  cmbr3  31636  cmcm  31642  cmcm3  31643  pjch1  31698  pjch  31722  pj11  31742  pjnel  31754  eigorth  31866  elnlfn  31956  nmlnop0  32026  lnopeq  32037  lnopcon  32063  lnfncon  32084  pjdifnormi  32195  chrelat2  32398  cvexch  32402  mdsym  32440  eqelbid  32502  fmptcof2  32673  mgcoval  32960  mgcval  32961  mgccole1  32964  mgccole2  32965  mgcmnt1  32966  mgcmnt2  32967  mgccnv  32973  unitprodclb  33396  ist0cld  33793  zarclssn  33833  zart0  33839  signswch  34554  fnrelpredd  35081  cvmlift2lem12  35298  cvmlift2lem13  35299  satfv1lem  35346  satf0op  35361  fmlafvel  35369  abs2sqle  35664  abs2sqlt  35665  axextdist  35780  brimageg  35908  brdomaing  35916  brrangeg  35917  elhf2  36156  nn0prpwlem  36304  nn0prpw  36305  onsuct0  36423  bj-sbceqgALT  36884  bj-elabd2ALT  36907  eleq2w2ALT  37029  dfgcd3  37306  cbveud  37354  wl-3xorbi123d  37457  matunitlindf  37604  prdsbnd2  37781  isdrngo1  37942  eqrelf  38236  elsymrels5  38537  dfdisjs5  38693  eldisjs5  38707  mpets2  38822  pets  38833  lsatcmp  38984  llnexchb2  39851  lautset  40064  lautle  40066  sticksstones2  42128  aks6d1c7  42165  dvdsexpnn0  42347  eu6w  42662  abbibw  42663  zindbi  42934  wepwsolem  43030  aomclem8  43049  onsupmaxb  43227  oaordnr  43285  omnord1  43294  oenord1  43305  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  2sbc6g  44410  2sbc5g  44411  modelaxreplem3  44944  wessf1ornlem  45127  fourierdlem31  46093  fourierdlem42  46104  fourierdlem54  46115  funressndmafv2rn  47172  dfatbrafv2b  47194  fnbrafv2b  47197  ichbidv  47377  ichnfim  47388  sprsymrelf  47419  sprsymrelfo  47421  isuspgrimlem  47811  line2ylem  48600  line2xlem  48602  mofeu  48677  catprslem  48798