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  4397  fnprb  7211  fntpb  7212  eqfunresadj  7363  eloprabga  7525  ordsucuniel  7827  ordsucun  7828  oeoa  8618  ereldm  8778  boxcutc  8964  mapen  9164  mapfien  9431  wemapwe  9720  sdom2en01  10325  prlem936  11070  subcan  11547  mulcan1g  11899  conjmul  11967  ltrec  12133  rebtwnz  12972  xposdif  13287  divelunit  13517  fseq1m1p1  13622  fzm1  13630  fllt  13829  hashfacen  14476  hashf1  14479  ccat0  14597  lenegsq  15342  dvdsmod  16349  bitsmod  16456  smueqlem  16510  rpexp  16742  eulerthlem2  16802  odzdvds  16816  pcelnn  16891  xpsle  17600  isepi  17760  fthmon  17950  cat1  18118  pospropd  18346  grpidpropd  18649  mgmhmpropd  18685  sgrppropd  18718  mndpropd  18746  mhmpropd  18779  grppropd  18943  ghmnsgima  19232  mndodcong  19533  odf1  19553  odf1o1  19563  sylow3lem6  19623  lsmcntzr  19671  efgredlema  19731  cmnpropd  19782  qusecsub  19826  dprdf11  20016  rngpropd  20144  ringpropd  20258  dvdsrpropd  20389  resrhm2b  20575  abvpropd  20809  lmodprop2d  20895  lsspropd  20989  lmhmpropd  21045  lbspropd  21071  lvecvscan  21086  lvecvscan2  21087  chrnzr  21512  zndvds0  21536  ip2eq  21638  phlpropd  21640  assapropd  21859  qtopcn  23687  tsmsf1o  24118  xmetgt0  24332  txmetcnp  24523  metustsym  24531  nlmmul0or  24659  cnmet  24747  evth  24946  isclmp  25085  minveclem3b  25417  mbfposr  25642  itg2cn  25753  iblcnlem  25779  dvcvx  26014  ulm2  26383  efeq1  26525  dcubic  26844  mcubic  26845  dquart  26851  birthdaylem3  26951  ftalem2  27072  issqf  27134  sqff1o  27180  bposlem7  27289  lgsabs1  27335  gausslemma2dlem1a  27364  lgsquadlem2  27380  addsq2reu  27439  dchrisum0lem1  27515  sltrec  27820  opphllem6  28715  colhp  28733  lmiinv  28755  lmiopp  28765  wlkeq  29599  eupth2lem3lem3  30196  eupth2lem3lem6  30199  nmounbi  30742  ip2eqi  30822  hvmulcan  31038  hvsubcan2  31041  hi2eq  31071  fh2  31585  riesz4i  32029  cvbr4i  32333  xdivpnfrp  32862  isorng  33275  qusker  33318  ellspds  33337  ply1moneq  33552  ballotlemfc0  34436  ballotlemfcc  34437  sgnmulsgn  34493  sgnmulsgp  34494  subfacp1lem5  35130  topfneec2  36298  neibastop3  36304  unccur  37551  cos2h  37559  tan2h  37560  poimirlem25  37593  poimirlem27  37595  dvasin  37652  caures  37708  ismtyima  37751  isdmn3  38022  dmecd  38246  releldmqscoss  38602  tendospcanN  40966  dochsncom  41325  f1o2d2  42214  sqrtcval  43599  or3or  43981  neicvgel1  44077  rusbcALT  44403  sbcoreleleqVD  44824  climreeq  45573  coseq0  45824  affinecomb1  48569  eenglngeehlnmlem1  48604  2sphere  48616  line2  48619  itscnhlc0yqe  48626  itscnhlc0xyqsol  48632  oduoppcciso  49159