Theorem 3bitr3d 308

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 280	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 278	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbcne12  4411  fnprb  7211  fntpb  7212  eqfunresadj  7359  eloprabga  7518  eloprabgaOLD  7519  ordsucuniel  7814  ordsucun  7815  oeoa  8599  ereldm  8753  boxcutc  8937  mapen  9143  mapfien  9405  wemapwe  9694  sdom2en01  10299  prlem936  11044  subcan  11519  mulcan1g  11871  conjmul  11935  ltrec  12100  rebtwnz  12935  xposdif  13245  divelunit  13475  fseq1m1p1  13580  fzm1  13585  fllt  13775  hashfacen  14417  hashfacenOLD  14418  hashf1  14422  ccat0  14530  lenegsq  15271  dvdsmod  16276  bitsmod  16381  smueqlem  16435  rpexp  16663  eulerthlem2  16719  odzdvds  16732  pcelnn  16807  xpsle  17529  isepi  17691  fthmon  17882  cat1  18051  pospropd  18284  grpidpropd  18587  mgmhmpropd  18623  sgrppropd  18656  mndpropd  18684  mhmpropd  18714  grppropd  18873  ghmnsgima  19154  mndodcong  19451  odf1  19471  odf1o1  19481  sylow3lem6  19541  lsmcntzr  19589  efgredlema  19649  cmnpropd  19700  qusecsub  19744  dprdf11  19934  rngpropd  20068  ringpropd  20176  dvdsrpropd  20307  resrhm2b  20492  abvpropd  20593  lmodprop2d  20678  lsspropd  20772  lmhmpropd  20828  lbspropd  20854  lvecvscan  20869  lvecvscan2  20870  chrnzr  21301  zndvds0  21325  ip2eq  21425  phlpropd  21427  assapropd  21645  qtopcn  23438  tsmsf1o  23869  xmetgt0  24084  txmetcnp  24276  metustsym  24284  nlmmul0or  24420  cnmet  24508  evth  24705  isclmp  24844  minveclem3b  25176  mbfposr  25401  itg2cn  25513  iblcnlem  25538  dvcvx  25772  ulm2  26133  efeq1  26273  dcubic  26587  mcubic  26588  dquart  26594  birthdaylem3  26694  ftalem2  26814  issqf  26876  sqff1o  26922  bposlem7  27029  lgsabs1  27075  gausslemma2dlem1a  27104  lgsquadlem2  27120  addsq2reu  27179  dchrisum0lem1  27255  sltrec  27558  opphllem6  28270  colhp  28288  lmiinv  28310  lmiopp  28320  wlkeq  29158  eupth2lem3lem3  29750  eupth2lem3lem6  29753  nmounbi  30296  ip2eqi  30376  hvmulcan  30592  hvsubcan2  30595  hi2eq  30625  fh2  31139  riesz4i  31583  cvbr4i  31887  xdivpnfrp  32366  isorng  32687  qusker  32734  ellspds  32755  ply1moneq  32939  ballotlemfc0  33789  ballotlemfcc  33790  sgnmulsgn  33846  sgnmulsgp  33847  subfacp1lem5  34473  topfneec2  35544  neibastop3  35550  unccur  36774  cos2h  36782  tan2h  36783  poimirlem25  36816  poimirlem27  36818  dvasin  36875  caures  36931  ismtyima  36974  isdmn3  37245  dmecd  37476  releldmqscoss  37833  tendospcanN  40197  dochsncom  40556  f1o2d2  41361  sqrtcval  42694  or3or  43076  neicvgel1  43172  rusbcALT  43500  sbcoreleleqVD  43922  climreeq  44627  coseq0  44878  affinecomb1  47475  eenglngeehlnmlem1  47510  2sphere  47522  line2  47525  itscnhlc0yqe  47532  itscnhlc0xyqsol  47538