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  1525  norass  1537  ru0  2128  sbbib  2360  sb8eulem  2592  abbib  2799  cleqh  2858  cleqf  2921  vtoclbg  3526  vtoclb  3537  ceqsexg  3622  elabgf  3644  reu6  3700  ruOLD  3755  sbcbig  3808  unineq  4254  sbcnestgfw  4387  sbcnestgf  4392  preq12bg  4820  axrep1  5238  axrep4OLD  5244  nalset  5271  opthg  5440  opelopabsb  5493  isso2i  5586  opeliunxp2  5805  resieq  5964  dfpo2  6272  cbviotaw  6474  cbviota  6476  iota2df  6501  fnbrfvb  6914  fvelimab  6936  fvopab5  7004  fmptco  7104  fsng  7112  fressnfv  7135  fnpr2g  7187  isorel  7304  isocnv  7308  isocnv3  7310  isotr  7314  eqfunresadj  7338  ovg  7557  caovcang  7593  caovordg  7599  caovord3d  7602  caovord  7603  caofidlcan  7694  orduninsuc  7822  xpord2pred  8127  xpord3pred  8134  opeliunxp2f  8192  brtpos  8217  dftpos4  8227  omopth  8629  ecopovsym  8795  xpf1o  9109  nneneq  9176  ttrclselem2  9686  r1pwALT  9806  karden  9855  infxpenlem  9973  aceq0  10078  cflim2  10223  zfac  10420  ttukeylem1  10469  axextnd  10551  axrepndlem1  10552  axrepndlem2  10553  axrepnd  10554  axacndlem5  10571  zfcndrep  10574  zfcndac  10579  winalim  10655  gruina  10778  ltrnq  10939  ltsosr  11054  ltasr  11060  axpre-lttri  11125  axpre-ltadd  11127  nn0sub  12499  zextle  12614  zextlt  12615  xlesubadd  13230  sqeqor  14188  nn0opth2  14244  rexfiuz  15321  climshft  15549  rpnnen2lem10  16198  dvdsext  16298  ltoddhalfle  16338  halfleoddlt  16339  sumodd  16365  sadcadd  16435  dvdssq  16544  rpexp  16699  pcdvdsb  16847  imasleval  17511  isacs2  17621  acsfiel  17622  funcres2b  17866  pospropd  18293  isnsg  19094  nsgbi  19096  elnmz  19102  nmzbi  19103  oddvdsnn0  19481  odeq  19487  odmulg  19493  isslw  19545  slwispgp  19548  gsumval3lem2  19843  gsumcom2  19912  abveq0  20734  cnt0  23240  kqfvima  23624  kqt0lem  23630  isr0  23631  r0cld  23632  regr1lem2  23634  nrmr0reg  23643  isfildlem  23751  cnextfvval  23959  xmeteq0  24233  imasf1oxmet  24270  comet  24408  dscmet  24467  nrmmetd  24469  tngngp  24549  tngngp3  24551  mbfsup  25572  mbfinf  25573  degltlem1  25984  logltb  26516  cxple2  26613  rlimcnp  26882  rlimcnp2  26883  isppw2  27032  sqf11  27056  slerec  27738  tgjustc1  28409  tgjustc2  28410  f1otrgitv  28804  nbuhgr2vtx1edgb  29286  dfconngr1  30124  eupth2lem3lem6  30169  nmlno0i  30730  nmlno0  30731  blocn  30743  ubth  30809  hvsubeq0  31004  hvaddcan  31006  hvsubadd  31013  normsub0  31072  hlim2  31128  pjoc1  31370  pjoc2  31375  chne0  31430  chsscon3  31436  chlejb1  31448  chnle  31450  h1de2ci  31492  elspansn  31502  elspansn2  31503  cmbr3  31544  cmcm  31550  cmcm3  31551  pjch1  31606  pjch  31630  pj11  31650  pjnel  31662  eigorth  31774  elnlfn  31864  nmlnop0  31934  lnopeq  31945  lnopcon  31971  lnfncon  31992  pjdifnormi  32103  chrelat2  32306  cvexch  32310  mdsym  32348  eqelbid  32411  fmptcof2  32588  mgcoval  32919  mgcval  32920  mgccole1  32923  mgccole2  32924  mgcmnt1  32925  mgcmnt2  32926  mgccnv  32932  unitprodclb  33367  ist0cld  33830  zarclssn  33870  zart0  33876  signswch  34559  fnrelpredd  35086  cvmlift2lem12  35308  cvmlift2lem13  35309  satfv1lem  35356  satf0op  35371  fmlafvel  35379  abs2sqle  35674  abs2sqlt  35675  axextdist  35794  brimageg  35922  brdomaing  35930  brrangeg  35931  elhf2  36170  nn0prpwlem  36317  nn0prpw  36318  onsuct0  36436  bj-sbceqgALT  36897  bj-elabd2ALT  36920  eleq2w2ALT  37042  dfgcd3  37319  cbveud  37367  wl-3xorbi123d  37470  matunitlindf  37619  prdsbnd2  37796  isdrngo1  37957  eqrelf  38251  elsymrels5  38554  dfdisjs5  38711  eldisjs5  38725  mpets2  38840  pets  38851  lsatcmp  39003  llnexchb2  39870  lautset  40083  lautle  40085  sticksstones2  42142  aks6d1c7  42179  dvdsexpnn0  42329  eu6w  42671  abbibw  42672  zindbi  42942  wepwsolem  43038  aomclem8  43057  onsupmaxb  43235  oaordnr  43292  omnord1  43301  oenord1  43312  ntrneik13  44094  ntrneix13  44095  ntrneik4w  44096  2sbc6g  44411  2sbc5g  44412  modelaxreplem3  44977  wessf1ornlem  45186  fourierdlem31  46143  fourierdlem42  46154  fourierdlem54  46165  funressndmafv2rn  47228  dfatbrafv2b  47250  fnbrafv2b  47253  ichbidv  47458  ichnfim  47469  sprsymrelf  47500  sprsymrelfo  47502  isuspgrimlem  47899  line2ylem  48744  line2xlem  48746  mofeu  48840  tposres0  48869  catprslem  49003