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  4369  fnprb  7164  fntpb  7165  eqfunresadj  7316  eloprabga  7477  ordsucuniel  7776  ordsucun  7777  oeoa  8535  ereldm  8699  boxcutc  8891  mapen  9081  mapfien  9323  wemapwe  9618  sdom2en01  10224  prlem936  10970  subcan  11448  mulcan1g  11802  conjmul  11870  ltrec  12036  rebtwnz  12872  xposdif  13189  divelunit  13422  fseq1m1p1  13527  fzm1  13535  fllt  13738  hashfacen  14389  hashf1  14392  ccat0  14511  lenegsq  15256  dvdsmod  16268  bitsmod  16375  smueqlem  16429  rpexp  16661  eulerthlem2  16721  odzdvds  16735  pcelnn  16810  xpsle  17512  isepi  17676  fthmon  17865  cat1  18033  pospropd  18260  grpidpropd  18599  mgmhmpropd  18635  sgrppropd  18668  mndpropd  18696  mhmpropd  18729  grppropd  18893  ghmnsgima  19181  mndodcong  19483  odf1  19503  odf1o1  19513  sylow3lem6  19573  lsmcntzr  19621  efgredlema  19681  cmnpropd  19732  qusecsub  19776  dprdf11  19966  rngpropd  20121  ringpropd  20235  dvdsrpropd  20364  resrhm2b  20547  abvpropd  20780  isorng  20806  lmodprop2d  20887  lsspropd  20981  lmhmpropd  21037  lbspropd  21063  lvecvscan  21078  lvecvscan2  21079  chrnzr  21497  zndvds0  21517  ip2eq  21620  phlpropd  21622  assapropd  21839  qtopcn  23670  tsmsf1o  24101  xmetgt0  24314  txmetcnp  24503  metustsym  24511  nlmmul0or  24639  cnmet  24727  evth  24926  isclmp  25065  minveclem3b  25396  mbfposr  25621  itg2cn  25732  iblcnlem  25758  dvcvx  25993  ulm2  26362  efeq1  26505  dcubic  26824  mcubic  26825  dquart  26831  birthdaylem3  26931  ftalem2  27052  issqf  27114  sqff1o  27160  bposlem7  27269  lgsabs1  27315  gausslemma2dlem1a  27344  lgsquadlem2  27360  addsq2reu  27419  dchrisum0lem1  27495  sltssnb  27777  ltsrec  27809  opphllem6  28836  colhp  28854  lmiinv  28876  lmiopp  28886  wlkeq  29719  eupth2lem3lem3  30317  eupth2lem3lem6  30320  nmounbi  30863  ip2eqi  30943  hvmulcan  31159  hvsubcan2  31162  hi2eq  31192  fh2  31706  riesz4i  32150  cvbr4i  32454  sgnmulsgn  32933  sgnmulsgp  32934  xdivpnfrp  33024  qusker  33441  ellspds  33460  ply1moneq  33680  ballotlemfc0  34670  ballotlemfcc  34671  subfacp1lem5  35397  topfneec2  36569  neibastop3  36575  unccur  37843  cos2h  37851  tan2h  37852  poimirlem25  37885  poimirlem27  37887  dvasin  37944  caures  38000  ismtyima  38043  isdmn3  38314  dmecd  38550  releldmqscoss  38985  tendospcanN  41388  dochsncom  41747  f1o2d2  42594  sqrtcval  43986  or3or  44368  neicvgel1  44464  rusbcALT  44783  sbcoreleleqVD  45203  climreeq  45962  coseq0  46211  modmkpkne  47710  affinecomb1  49051  eenglngeehlnmlem1  49086  2sphere  49098  line2  49101  itscnhlc0yqe  49108  itscnhlc0xyqsol  49114  oduoppcciso  49914