Theorem 3bitr3d 309

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

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

Assertion

Ref	Expression
3bitr3d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr3d 281	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 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:  sbcne12  4366  fnprb  7151  fntpb  7152  eqfunresadj  7303  eloprabga  7464  ordsucuniel  7763  ordsucun  7764  oeoa  8521  ereldm  8684  boxcutc  8874  mapen  9064  mapfien  9302  wemapwe  9597  sdom2en01  10203  prlem936  10948  subcan  11426  mulcan1g  11780  conjmul  11848  ltrec  12014  rebtwnz  12855  xposdif  13171  divelunit  13404  fseq1m1p1  13509  fzm1  13517  fllt  13720  hashfacen  14371  hashf1  14374  ccat0  14493  lenegsq  15238  dvdsmod  16250  bitsmod  16357  smueqlem  16411  rpexp  16643  eulerthlem2  16703  odzdvds  16717  pcelnn  16792  xpsle  17493  isepi  17657  fthmon  17846  cat1  18014  pospropd  18241  grpidpropd  18580  mgmhmpropd  18616  sgrppropd  18649  mndpropd  18677  mhmpropd  18710  grppropd  18874  ghmnsgima  19162  mndodcong  19464  odf1  19484  odf1o1  19494  sylow3lem6  19554  lsmcntzr  19602  efgredlema  19662  cmnpropd  19713  qusecsub  19757  dprdf11  19947  rngpropd  20102  ringpropd  20216  dvdsrpropd  20344  resrhm2b  20527  abvpropd  20760  isorng  20786  lmodprop2d  20867  lsspropd  20961  lmhmpropd  21017  lbspropd  21043  lvecvscan  21058  lvecvscan2  21059  chrnzr  21477  zndvds0  21497  ip2eq  21600  phlpropd  21602  assapropd  21819  qtopcn  23639  tsmsf1o  24070  xmetgt0  24283  txmetcnp  24472  metustsym  24480  nlmmul0or  24608  cnmet  24696  evth  24895  isclmp  25034  minveclem3b  25365  mbfposr  25590  itg2cn  25701  iblcnlem  25727  dvcvx  25962  ulm2  26331  efeq1  26474  dcubic  26793  mcubic  26794  dquart  26800  birthdaylem3  26900  ftalem2  27021  issqf  27083  sqff1o  27129  bposlem7  27238  lgsabs1  27284  gausslemma2dlem1a  27313  lgsquadlem2  27329  addsq2reu  27388  dchrisum0lem1  27464  ssltsnb  27742  sltrec  27772  opphllem6  28740  colhp  28758  lmiinv  28780  lmiopp  28790  wlkeq  29623  eupth2lem3lem3  30221  eupth2lem3lem6  30224  nmounbi  30767  ip2eqi  30847  hvmulcan  31063  hvsubcan2  31066  hi2eq  31096  fh2  31610  riesz4i  32054  cvbr4i  32358  sgnmulsgn  32836  sgnmulsgp  32837  xdivpnfrp  32924  qusker  33325  ellspds  33344  ply1moneq  33561  ballotlemfc0  34517  ballotlemfcc  34518  subfacp1lem5  35239  topfneec2  36411  neibastop3  36417  unccur  37653  cos2h  37661  tan2h  37662  poimirlem25  37695  poimirlem27  37697  dvasin  37754  caures  37810  ismtyima  37853  isdmn3  38124  dmecd  38352  releldmqscoss  38768  tendospcanN  41132  dochsncom  41491  f1o2d2  42341  sqrtcval  43748  or3or  44130  neicvgel1  44226  rusbcALT  44545  sbcoreleleqVD  44965  climreeq  45727  coseq0  45976  modmkpkne  47475  affinecomb1  48817  eenglngeehlnmlem1  48852  2sphere  48864  line2  48867  itscnhlc0yqe  48874  itscnhlc0xyqsol  48880  oduoppcciso  49681