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 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bi2bian9  651  xorbi12d  1548  norass  1560  ru0  2164  sbbib  2395  sb8eulem  2628  abbib  2834  cleqh  2894  cleqf  2955  vtoclbg  3527  vtoclb  3536  ceqsexg  3615  elabgf  3636  reu6  3692  sbcbig  3798  unineq  4243  sbcnestgfw  4378  sbcnestgf  4383  preq12bg  4814  axrep1  5233  axrep4OLD  5239  nalsetOLD  5270  opthg  5450  opelopabsb  5505  isso2i  5597  opeliunxp2  5815  resieq  5980  dfpo2  6287  cbviotaw  6488  cbviota  6490  iota2df  6512  fnbrfvb  6921  fvelimab  6943  fvopab5  7013  fmptco  7115  fsng  7123  fressnfv  7147  fnpr2g  7198  isorel  7314  isocnv  7318  isocnv3  7320  isotr  7324  eqfunresadj  7348  ovg  7565  caovcang  7601  caovordg  7607  caovord3d  7610  caovord  7611  caofidlcan  7702  orduninsuc  7827  xpord2pred  8129  xpord3pred  8136  opeliunxp2f  8194  brtpos  8219  dftpos4  8229  omopth  8636  ecopovsym  8805  xpf1o  9115  nneneq  9178  ttrclselem2  9683  r1pwALT  9806  karden  9869  infxpenlem  9985  aceq0  10090  cflim2  10235  zfac  10432  ttukeylem1  10481  axextnd  10564  axrepndlem1  10565  axrepndlem2  10566  axrepnd  10567  axacndlem5  10584  zfcndrep  10587  zfcndac  10592  winalim  10668  gruina  10791  ltrnq  10952  ltsosr  11067  ltasr  11073  axpre-lttri  11138  axpre-ltadd  11140  nn0sub  12545  zextle  12660  zextlt  12661  xlesubadd  13280  sqeqor  14243  nn0opth2  14299  rexfiuz  15389  climshft  15617  rpnnen2lem10  16269  dvdsext  16369  ltoddhalfle  16409  halfleoddlt  16410  sumodd  16436  sadcadd  16506  dvdssq  16615  rpexp  16771  pcdvdsb  16919  imasleval  17585  isacs2  17699  acsfiel  17700  funcres2b  17944  pospropd  18371  isnsg  19212  nsgbi  19214  elnmz  19220  nmzbi  19221  oddvdsnn0  19605  odeq  19611  odmulg  19617  isslw  19669  slwispgp  19672  gsumval3lem2  19967  gsumcom2  20036  abveq0  20890  cnt0  23464  kqfvima  23848  kqt0lem  23854  isr0  23855  r0cld  23856  regr1lem2  23858  nrmr0reg  23867  isfildlem  23975  cnextfvval  24183  xmeteq0  24456  imasf1oxmet  24493  comet  24631  dscmet  24690  nrmmetd  24692  tngngp  24772  tngngp3  24774  mbfsup  25784  mbfinf  25785  degltlem1  26190  logltb  26723  cxple2  26820  rlimcnp  27088  rlimcnp2  27089  isppw2  27237  sqf11  27261  lesrec  27950  tgjustc1  28702  tgjustc2  28703  f1otrgitv  29128  nbuhgr2vtx1edgb  29611  dfconngr1  30448  eupth2lem3lem6  30493  nmlno0i  31055  nmlno0  31056  blocn  31068  ubth  31134  hvsubeq0  31329  hvaddcan  31331  hvsubadd  31338  normsub0  31397  hlim2  31453  pjoc1  31695  pjoc2  31700  chne0  31755  chsscon3  31761  chlejb1  31773  chnle  31775  h1de2ci  31817  elspansn  31827  elspansn2  31828  cmbr3  31869  cmcm  31875  cmcm3  31876  pjch1  31931  pjch  31955  pj11  31975  pjnel  31987  eigorth  32099  elnlfn  32189  nmlnop0  32259  lnopeq  32270  lnopcon  32296  lnfncon  32317  pjdifnormi  32428  chrelat2  32631  cvexch  32635  mdsym  32673  eqelbid  32731  fmptcof2  32914  mgcoval  33219  mgcval  33220  mgccole1  33223  mgccole2  33224  mgcmnt1  33225  mgcmnt2  33226  mgccnv  33232  domnprodeq0  33512  unitprodclb  33618  ist0cld  34140  zarclssn  34180  zart0  34186  signswch  34865  fnrelpredd  35397  r1omhfb  35420  r1omhfbregs  35445  axsepg2  35448  axsepg4  35451  cvmlift2lem12  35677  cvmlift2lem13  35678  satfv1lem  35725  satf0op  35740  fmlafvel  35748  abs2sqle  36043  abs2sqlt  36044  axextdist  36160  brimageg  36288  brdomaing  36296  brrangeg  36297  elhf2  36538  nn0prpwlem  36695  nn0prpw  36696  onsuct0  36814  ttcwf2  36898  bj-sbceqgALT  37399  bj-elabd2ALT  37422  eleq2w2ALT  37544  bj-axseprep  37571  dfgcd3  37828  cbveud  37878  wl-3xorbi123d  37981  wl-dfcleq  38020  matunitlindf  38129  prdsbnd2  38306  isdrngo1  38467  eqrelf  38769  elsymrels5  39151  dfdisjs5  39308  eldisjs5  39334  mpets2  39466  pets  39477  lsatcmp  39639  llnexchb2  40505  lautset  40718  lautle  40720  sticksstones2  42776  aks6d1c7  42813  dvdsexpnn0  42955  eu6w  43270  abbibw  43271  zindbi  43535  wepwsolem  43631  aomclem8  43650  onsupmaxb  43828  oaordnr  43885  omnord1  43894  oenord1  43905  ntrneik13  44686  ntrneix13  44687  ntrneik4w  44688  2sbc6g  44989  2sbc5g  44990  modelaxreplem3  45554  wessf1ornlem  45761  fourierdlem31  46710  fourierdlem42  46721  fourierdlem54  46732  funressndmafv2rn  47815  dfatbrafv2b  47837  fnbrafv2b  47840  ichbidv  48057  ichnfim  48068  sprsymrelf  48099  sprsymrelfo  48101  isuspgrimlem  48515  line2ylem  49382  line2xlem  49384  mofeu  49477  tposres0  49506  catprslem  49639