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  4368  fnprb  7148  fntpb  7149  eqfunresadj  7301  eloprabga  7462  ordsucuniel  7763  ordsucun  7764  oeoa  8522  ereldm  8685  boxcutc  8875  mapen  9065  mapfien  9317  wemapwe  9612  sdom2en01  10215  prlem936  10960  subcan  11437  mulcan1g  11791  conjmul  11859  ltrec  12025  rebtwnz  12866  xposdif  13182  divelunit  13415  fseq1m1p1  13520  fzm1  13528  fllt  13728  hashfacen  14379  hashf1  14382  ccat0  14501  lenegsq  15246  dvdsmod  16258  bitsmod  16365  smueqlem  16419  rpexp  16651  eulerthlem2  16711  odzdvds  16725  pcelnn  16800  xpsle  17501  isepi  17665  fthmon  17854  cat1  18022  pospropd  18249  grpidpropd  18554  mgmhmpropd  18590  sgrppropd  18623  mndpropd  18651  mhmpropd  18684  grppropd  18848  ghmnsgima  19137  mndodcong  19439  odf1  19459  odf1o1  19469  sylow3lem6  19529  lsmcntzr  19577  efgredlema  19637  cmnpropd  19688  qusecsub  19732  dprdf11  19922  rngpropd  20077  ringpropd  20191  dvdsrpropd  20319  resrhm2b  20505  abvpropd  20738  isorng  20764  lmodprop2d  20845  lsspropd  20939  lmhmpropd  20995  lbspropd  21021  lvecvscan  21036  lvecvscan2  21037  chrnzr  21455  zndvds0  21475  ip2eq  21578  phlpropd  21580  assapropd  21797  qtopcn  23617  tsmsf1o  24048  xmetgt0  24262  txmetcnp  24451  metustsym  24459  nlmmul0or  24587  cnmet  24675  evth  24874  isclmp  25013  minveclem3b  25344  mbfposr  25569  itg2cn  25680  iblcnlem  25706  dvcvx  25941  ulm2  26310  efeq1  26453  dcubic  26772  mcubic  26773  dquart  26779  birthdaylem3  26879  ftalem2  27000  issqf  27062  sqff1o  27108  bposlem7  27217  lgsabs1  27263  gausslemma2dlem1a  27292  lgsquadlem2  27308  addsq2reu  27367  dchrisum0lem1  27443  sltrec  27750  opphllem6  28715  colhp  28733  lmiinv  28755  lmiopp  28765  wlkeq  29597  eupth2lem3lem3  30192  eupth2lem3lem6  30195  nmounbi  30738  ip2eqi  30818  hvmulcan  31034  hvsubcan2  31037  hi2eq  31067  fh2  31581  riesz4i  32025  cvbr4i  32329  sgnmulsgn  32800  sgnmulsgp  32801  xdivpnfrp  32886  qusker  33296  ellspds  33315  ply1moneq  33531  ballotlemfc0  34460  ballotlemfcc  34461  subfacp1lem5  35156  topfneec2  36329  neibastop3  36335  unccur  37582  cos2h  37590  tan2h  37591  poimirlem25  37624  poimirlem27  37626  dvasin  37683  caures  37739  ismtyima  37782  isdmn3  38053  dmecd  38277  releldmqscoss  38637  tendospcanN  41002  dochsncom  41361  f1o2d2  42206  sqrtcval  43614  or3or  43996  neicvgel1  44092  rusbcALT  44412  sbcoreleleqVD  44832  climreeq  45595  coseq0  45846  modmkpkne  47346  affinecomb1  48675  eenglngeehlnmlem1  48710  2sphere  48722  line2  48725  itscnhlc0yqe  48732  itscnhlc0xyqsol  48738  oduoppcciso  49539