Theorem bibi12d 348

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 346	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 345	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 282	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bi2bian9  652  xorbi12d  1554  norass  1566  ru0  2163  sbbib  2390  sb8eulem  2623  abbib  2829  cleqh  2889  cleqf  2950  vtoclbg  3519  vtoclb  3528  ceqsexg  3606  elabgf  3627  reu6  3683  sbcbig  3789  unineq  4233  sbcnestgfw  4378  sbcnestgf  4383  preq12bg  4807  axrep1  5232  nalsetOLD  5268  opthg  5445  opelopabsb  5503  isso2i  5595  opeliunxp2  5814  resieq  5980  dfpo2  6299  cbviotaw  6501  cbviota  6503  iota2df  6525  fnbrfvb  6936  fvelimab  6958  fvopab5  7028  fmptco  7131  fsng  7139  fressnfv  7165  fnpr2g  7217  isorel  7335  isocnv  7339  isocnv3  7341  isotr  7345  eqfunresadj  7371  ovg  7586  caovcang  7623  caovordg  7629  caovord3d  7632  caovord  7633  caofidlcan  7732  orduninsuc  7855  xpord2pred  8165  xpord3pred  8172  opeliunxp2f  8231  brtpos  8256  dftpos4  8266  omopth  8675  ecopovsym  8844  xpf1o  9162  nneneq  9225  ttrclselem2  9731  r1pwALT  9864  elhf2  9914  kardenOLD  9964  infxpenlem  10096  aceq0  10201  cflim2  10345  zfac  10542  ttukeylem1  10591  axextnd  10680  axrepndlem1  10681  axrepndlem2  10682  axrepnd  10683  axacndlem5  10700  zfcndrep  10703  zfcndac  10708  winalim  10784  gruina  10907  ltrnq  11068  ltsosr  11183  ltasr  11189  axpre-lttri  11254  axpre-ltadd  11256  nn0sub  12660  zextle  12776  zextlt  12777  xlesubadd  13397  sqeqor  14364  nn0opth2  14420  rexfiuz  15521  climshft  15749  rpnnen2lem10  16397  dvdsext  16497  ltoddhalfle  16537  halfleoddlt  16538  sumodd  16564  sadcadd  16634  dvdssq  16748  rpexp  16904  pcdvdsb  17053  imasleval  17719  isacs2  17833  acsfiel  17834  funcres2b  18078  pospropd  18505  isnsg  19371  nsgbi  19373  elnmz  19379  nmzbi  19380  oddvdsnn0  19764  odeq  19770  odmulg  19776  isslw  19828  slwispgp  19831  gsumval3lem2  20126  gsumcom2  20195  abveq0  21081  matunitlindf  23002  cnt0  23670  kqfvima  24055  kqt0lem  24061  isr0  24062  r0cld  24063  regr1lem2  24065  nrmr0reg  24074  isfildlem  24182  cnextfvval  24390  xmeteq0  24663  imasf1oxmet  24700  comet  24838  dscmet  24897  nrmmetd  24899  tngngp  24979  tngngp3  24981  mbfsup  25991  mbfinf  25992  degltlem1  26396  logltb  26934  cxple2  27031  rlimcnp  27299  rlimcnp2  27300  isppw2  27448  sqf11  27472  lesrec  28191  tgjustc1  28943  tgjustc2  28944  f1otrgitv  29453  nbuhgr2vtx1edgb  29939  dfconngr1  30795  eupth2lem3lem6  30840  nmlno0i  31402  nmlno0  31403  blocn  31415  ubth  31481  hvsubeq0  31676  hvaddcan  31678  hvsubadd  31685  normsub0  31744  hlim2  31800  pjoc1  32042  pjoc2  32047  chne0  32102  chsscon3  32108  chlejb1  32120  chnle  32122  h1de2ci  32164  elspansn  32174  elspansn2  32175  cmbr3  32216  cmcm  32222  cmcm3  32223  pjch1  32278  pjch  32302  pj11  32322  pjnel  32334  eigorth  32446  elnlfn  32536  nmlnop0  32606  lnopeq  32617  lnopcon  32643  lnfncon  32664  pjdifnormi  32775  chrelat2  32978  cvexch  32982  mdsym  33020  eqelbid  33119  fmptcof2  33299  mgcoval  33594  mgcval  33595  mgccole1  33598  mgccole2  33599  mgcmnt1  33600  mgcmnt2  33601  mgccnv  33607  domnprodeq0  33887  unitprodclb  33991  ist0cld  34512  zarclssn  34552  zart0  34558  signswch  35237  reu6f  35756  fnrelpredd  35773  r1omhfb  35791  r1omhfbregs  35862  axsepg2  35865  axsepg4  35868  cvmlift2lem12  36166  cvmlift2lem13  36167  satfv1lem  36214  satf0op  36229  fmlafvel  36237  abs2sqle  36532  abs2sqlt  36533  axextdist  36654  brimageg  36782  brdomaing  36790  brrangeg  36791  nn0prpwlem  37203  nn0prpw  37204  onsuct0  37322  ttcwf2  37406  bj-sbceqgALT  37907  bj-elabd2ALT  37931  eleq2w2ALT  38055  bj-axseprep  38083  dfgcd3  38339  cbveud  38389  wl-3xorbi123d  38492  wl-dfcleq  38531  prdsbnd2  38823  isdrngo1  38984  eqrelf  39284  elsymrels5  39666  dfdisjs5  39823  eldisjs5  39849  mpets2  39981  pets  39992  lsatcmp  40154  llnexchb2  41020  lautset  41233  lautle  41235  sticksstones2  43291  aks6d1c7  43328  dvdsexpnn0  43480  eu6w  43781  abbibw  43782  zindbi  44047  wepwsolem  44143  aomclem8  44157  onsupmaxb  44335  oaordnr  44392  omnord1  44401  oenord1  44412  ntrneik13  45192  ntrneix13  45193  ntrneik4w  45194  2sbc6g  45493  2sbc5g  45494  modelaxreplem3  46064  wessf1ornlem  46294  fourierdlem31  47242  fourierdlem42  47253  fourierdlem54  47264  funressndmafv2rn  48387  dfatbrafv2b  48409  fnbrafv2b  48412  ichbidv  48629  ichnfim  48640  sprsymrelf  48671  sprsymrelfo  48673  isuspgrimlem  49087  line2ylem  49957  line2xlem  49959  mofeu  50053  tposres0  50084  catprslem  50218