Theorem 3bitr3d 298

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  sbcne12  3986  fnprb  6472  fntpb  6473  eloprabga  6747  ordsucuniel  7024  ordsucun  7025  oeoa  7677  ereldm  7790  boxcutc  7951  mapen  8124  mapfien  8313  wemapwe  8594  sdom2en01  9124  prlem936  9869  subcan  10336  mulcan1g  10680  conjmul  10742  ltrec  10905  rebtwnz  11787  xposdif  12092  divelunit  12314  fseq1m1p1  12415  fzm1  12420  fllt  12607  hashfacen  13238  hashf1  13241  lenegsq  14060  dvdsmod  15050  bitsmod  15158  smueqlem  15212  rpexp  15432  eulerthlem2  15487  odzdvds  15500  pcelnn  15574  xpsle  16241  isepi  16400  fthmon  16587  pospropd  17134  grpidpropd  17261  mndpropd  17316  mhmpropd  17341  grppropd  17437  ghmnsgima  17684  mndodcong  17961  odf1  17979  odf1o1  17987  sylow3lem6  18047  lsmcntzr  18093  efgredlema  18153  cmnpropd  18202  dprdf11  18422  ringpropd  18582  dvdsrpropd  18696  abvpropd  18842  lmodprop2d  18925  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  lvecvscan  19111  lvecvscan2  19112  assapropd  19327  chrnzr  19878  zndvds0  19899  ip2eq  19998  phlpropd  20000  qtopcn  21517  tsmsf1o  21948  xmetgt0  22163  txmetcnp  22352  metustsym  22360  nlmmul0or  22487  cnmet  22575  evth  22758  isclmp  22897  minveclem3b  23199  mbfposr  23419  itg2cn  23530  iblcnlem  23555  dvcvx  23783  ulm2  24139  efeq1  24275  dcubic  24573  mcubic  24574  dquart  24580  birthdaylem3  24680  ftalem2  24800  issqf  24862  sqff1o  24908  bposlem7  25015  lgsabs1  25061  gausslemma2dlem1a  25090  lgsquadlem2  25106  dchrisum0lem1  25205  opphllem6  25644  colhp  25662  lmiinv  25684  lmiopp  25694  eupth2lem3lem3  27090  eupth2lem3lem6  27093  nmounbi  27631  ip2eqi  27712  hvmulcan  27929  hvsubcan2  27932  hi2eq  27962  fh2  28478  riesz4i  28922  cvbr4i  29226  xdivpnfrp  29641  isorng  29799  ballotlemfc0  30554  ballotlemfcc  30555  sgnmulsgn  30611  sgnmulsgp  30612  subfacp1lem5  31166  eqfunresadj  31659  sltrec  31924  topfneec2  32351  neibastop3  32357  unccur  33392  cos2h  33400  tan2h  33401  poimirlem25  33434  poimirlem27  33436  dvasin  33496  caures  33556  ismtyima  33602  isdmn3  33873  dmecd  34074  tendospcanN  36312  dochsncom  36671  or3or  38319  neicvgel1  38417  rusbcALT  38640  sbc3orgOLD  38742  climreeq  39845  coseq0  40075  mgmhmpropd  41785