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  4395  fnprb  7210  fntpb  7211  eqfunresadj  7362  eloprabga  7524  ordsucuniel  7826  ordsucun  7827  oeoa  8617  ereldm  8777  boxcutc  8963  mapen  9163  mapfien  9430  wemapwe  9719  sdom2en01  10324  prlem936  11069  subcan  11546  mulcan1g  11898  conjmul  11966  ltrec  12132  rebtwnz  12971  xposdif  13286  divelunit  13516  fseq1m1p1  13621  fzm1  13629  fllt  13828  hashfacen  14476  hashf1  14479  ccat0  14597  lenegsq  15342  dvdsmod  16349  bitsmod  16456  smueqlem  16510  rpexp  16742  eulerthlem2  16802  odzdvds  16816  pcelnn  16891  xpsle  17596  isepi  17756  fthmon  17946  cat1  18114  pospropd  18342  grpidpropd  18645  mgmhmpropd  18681  sgrppropd  18714  mndpropd  18742  mhmpropd  18775  grppropd  18939  ghmnsgima  19228  mndodcong  19529  odf1  19549  odf1o1  19559  sylow3lem6  19619  lsmcntzr  19667  efgredlema  19727  cmnpropd  19778  qusecsub  19822  dprdf11  20012  rngpropd  20140  ringpropd  20254  dvdsrpropd  20385  resrhm2b  20571  abvpropd  20805  lmodprop2d  20891  lsspropd  20985  lmhmpropd  21041  lbspropd  21067  lvecvscan  21082  lvecvscan2  21083  chrnzr  21504  zndvds0  21524  ip2eq  21626  phlpropd  21628  assapropd  21847  qtopcn  23669  tsmsf1o  24100  xmetgt0  24314  txmetcnp  24505  metustsym  24513  nlmmul0or  24641  cnmet  24729  evth  24928  isclmp  25067  minveclem3b  25399  mbfposr  25624  itg2cn  25735  iblcnlem  25761  dvcvx  25996  ulm2  26365  efeq1  26507  dcubic  26826  mcubic  26827  dquart  26833  birthdaylem3  26933  ftalem2  27054  issqf  27116  sqff1o  27162  bposlem7  27271  lgsabs1  27317  gausslemma2dlem1a  27346  lgsquadlem2  27362  addsq2reu  27421  dchrisum0lem1  27497  sltrec  27802  opphllem6  28697  colhp  28715  lmiinv  28737  lmiopp  28747  wlkeq  29581  eupth2lem3lem3  30178  eupth2lem3lem6  30181  nmounbi  30724  ip2eqi  30804  hvmulcan  31020  hvsubcan2  31023  hi2eq  31053  fh2  31567  riesz4i  32011  cvbr4i  32315  xdivpnfrp  32860  isorng  33274  qusker  33317  ellspds  33336  ply1moneq  33551  ballotlemfc0  34470  ballotlemfcc  34471  sgnmulsgn  34527  sgnmulsgp  34528  subfacp1lem5  35164  topfneec2  36332  neibastop3  36338  unccur  37585  cos2h  37593  tan2h  37594  poimirlem25  37627  poimirlem27  37629  dvasin  37686  caures  37742  ismtyima  37785  isdmn3  38056  dmecd  38280  releldmqscoss  38636  tendospcanN  41000  dochsncom  41359  f1o2d2  42248  sqrtcval  43631  or3or  44013  neicvgel1  44109  rusbcALT  44430  sbcoreleleqVD  44851  climreeq  45600  coseq0  45851  affinecomb1  48596  eenglngeehlnmlem1  48631  2sphere  48643  line2  48646  itscnhlc0yqe  48653  itscnhlc0xyqsol  48659  oduoppcciso  49258