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  1555  norass  1567  ru0  2165  sbbib  2396  sb8eulem  2629  abbib  2835  cleqh  2895  cleqf  2956  vtoclbg  3527  vtoclb  3536  ceqsexg  3615  elabgf  3636  reu6  3692  sbcbig  3798  unineq  4244  sbcnestgfw  4389  sbcnestgf  4394  preq12bg  4823  axrep1  5244  axrep4OLD  5250  nalsetOLD  5283  opthg  5464  opelopabsb  5519  isso2i  5611  opeliunxp2  5829  resieq  5994  dfpo2  6304  cbviotaw  6506  cbviota  6508  iota2df  6530  fnbrfvb  6938  fvelimab  6960  fvopab5  7030  fmptco  7132  fsng  7140  fressnfv  7164  fnpr2g  7215  isorel  7335  isocnv  7339  isocnv3  7341  isotr  7345  eqfunresadj  7371  ovg  7588  caovcang  7624  caovordg  7630  caovord3d  7633  caovord  7634  caofidlcan  7725  orduninsuc  7848  xpord2pred  8150  xpord3pred  8157  opeliunxp2f  8215  brtpos  8240  dftpos4  8250  omopth  8657  ecopovsym  8826  xpf1o  9137  nneneq  9200  ttrclselem2  9705  r1pwALT  9828  kardenOLD  9899  infxpenlem  10016  aceq0  10121  cflim2  10265  zfac  10462  ttukeylem1  10511  axextnd  10594  axrepndlem1  10595  axrepndlem2  10596  axrepnd  10597  axacndlem5  10614  zfcndrep  10617  zfcndac  10622  winalim  10698  gruina  10821  ltrnq  10982  ltsosr  11097  ltasr  11103  axpre-lttri  11168  axpre-ltadd  11170  nn0sub  12572  zextle  12687  zextlt  12688  xlesubadd  13307  sqeqor  14272  nn0opth2  14328  rexfiuz  15425  climshft  15653  rpnnen2lem10  16304  dvdsext  16404  ltoddhalfle  16444  halfleoddlt  16445  sumodd  16471  sadcadd  16541  dvdssq  16650  rpexp  16806  pcdvdsb  16954  imasleval  17620  isacs2  17734  acsfiel  17735  funcres2b  17979  pospropd  18406  isnsg  19252  nsgbi  19254  elnmz  19260  nmzbi  19261  oddvdsnn0  19645  odeq  19651  odmulg  19657  isslw  19709  slwispgp  19712  gsumval3lem2  20007  gsumcom2  20076  abveq0  20958  cnt0  23540  kqfvima  23924  kqt0lem  23930  isr0  23931  r0cld  23932  regr1lem2  23934  nrmr0reg  23943  isfildlem  24051  cnextfvval  24259  xmeteq0  24532  imasf1oxmet  24569  comet  24707  dscmet  24766  nrmmetd  24768  tngngp  24848  tngngp3  24850  mbfsup  25860  mbfinf  25861  degltlem1  26266  logltb  26802  cxple2  26899  rlimcnp  27167  rlimcnp2  27168  isppw2  27316  sqf11  27340  lesrec  28029  tgjustc1  28781  tgjustc2  28782  f1otrgitv  29256  nbuhgr2vtx1edgb  29739  dfconngr1  30576  eupth2lem3lem6  30621  nmlno0i  31183  nmlno0  31184  blocn  31196  ubth  31262  hvsubeq0  31457  hvaddcan  31459  hvsubadd  31466  normsub0  31525  hlim2  31581  pjoc1  31823  pjoc2  31828  chne0  31883  chsscon3  31889  chlejb1  31901  chnle  31903  h1de2ci  31945  elspansn  31955  elspansn2  31956  cmbr3  31997  cmcm  32003  cmcm3  32004  pjch1  32059  pjch  32083  pj11  32103  pjnel  32115  eigorth  32227  elnlfn  32317  nmlnop0  32387  lnopeq  32398  lnopcon  32424  lnfncon  32445  pjdifnormi  32556  chrelat2  32759  cvexch  32763  mdsym  32801  eqelbid  32858  fmptcof2  33039  mgcoval  33337  mgcval  33338  mgccole1  33341  mgccole2  33342  mgcmnt1  33343  mgcmnt2  33344  mgccnv  33350  domnprodeq0  33630  unitprodclb  33733  ist0cld  34254  zarclssn  34294  zart0  34300  signswch  34980  fnrelpredd  35507  r1omhfb  35533  r1omhfbregs  35574  axsepg2  35577  axsepg4  35580  cvmlift2lem12  35827  cvmlift2lem13  35828  satfv1lem  35875  satf0op  35890  fmlafvel  35898  abs2sqle  36193  abs2sqlt  36194  axextdist  36310  brimageg  36438  brdomaing  36446  brrangeg  36447  elhf2  36688  nn0prpwlem  36874  nn0prpw  36875  onsuct0  36993  ttcwf2  37077  bj-sbceqgALT  37578  bj-elabd2ALT  37602  eleq2w2ALT  37724  bj-axseprep  37752  dfgcd3  38009  cbveud  38059  wl-3xorbi123d  38162  wl-dfcleq  38201  matunitlindf  38310  prdsbnd2  38487  isdrngo1  38648  eqrelf  38948  elsymrels5  39330  dfdisjs5  39487  eldisjs5  39513  mpets2  39645  pets  39656  lsatcmp  39818  llnexchb2  40684  lautset  40897  lautle  40899  sticksstones2  42955  aks6d1c7  42992  dvdsexpnn0  43136  eu6w  43449  abbibw  43450  zindbi  43714  wepwsolem  43810  aomclem8  43829  onsupmaxb  44007  oaordnr  44064  omnord1  44073  oenord1  44084  ntrneik13  44865  ntrneix13  44866  ntrneik4w  44867  2sbc6g  45166  2sbc5g  45167  modelaxreplem3  45730  wessf1ornlem  45944  fourierdlem31  46893  fourierdlem42  46904  fourierdlem54  46915  funressndmafv2rn  48001  dfatbrafv2b  48023  fnbrafv2b  48026  ichbidv  48243  ichnfim  48254  sprsymrelf  48285  sprsymrelfo  48287  isuspgrimlem  48701  line2ylem  49572  line2xlem  49574  mofeu  49667  tposres0  49696  catprslem  49829