Theorem 3bitr3d 312

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbcne12  4383  fnprb  7213  fntpb  7214  eqfunresadj  7371  eloprabga  7532  ordsucuniel  7829  ordsucun  7830  mpof1o2d  8130  oeoa  8592  ereldm  8757  boxcutc  8948  mapen  9139  mapfien  9378  wemapwe  9676  sdom2en01  10304  prlem936  11050  subcan  11531  mulcan1g  11885  conjmul  11950  ltrec  12115  rebtwnz  12989  xposdif  13306  divelunit  13539  fseq1m1p1  13646  fzm1  13654  fllt  13859  hashfacen  14511  hashf1  14514  ccat0  14633  sgnmulsgn  15172  lenegsq  15398  dvdsmod  16412  bitsmod  16519  smueqlem  16573  rpexp  16806  eulerthlem2  16866  odzdvds  16880  pcelnn  16955  xpsle  17658  isepi  17822  fthmon  18011  cat1  18179  pospropd  18406  grpidpropd  18745  mgmhmpropd  18781  sgrppropd  18814  mndpropd  18842  mhmpropd  18875  grppropd  19043  ghmnsgima  19335  mndodcong  19637  odf1  19657  odf1o1  19667  sylow3lem6  19727  lsmcntzr  19775  efgredlema  19835  cmnpropd  19886  qusecsub  19930  dprdf11  20120  rngpropd  20277  ringpropd  20397  dvdsrpropd  20524  resrhm2b  20731  abvpropd  20968  isorng  20994  lmodprop2d  21075  lsspropd  21168  lmhmpropd  21224  lbspropd  21250  lvecvscan  21265  lvecvscan2  21266  chrnzr  21710  zndvds0  21730  ip2eq  21833  phlpropd  21835  assapropd  22051  qtopcn  23901  tsmsf1o  24332  xmetgt0  24545  txmetcnp  24734  metustsym  24742  nlmmul0or  24870  cnmet  24958  evth  25148  isclmp  25286  minveclem3b  25617  mbfposr  25841  itg2cn  25952  iblcnlem  25978  dvcvx  26209  ulm2  26578  efeq1  26723  dcubic  27041  mcubic  27042  dquart  27048  birthdaylem3  27148  ftalem2  27268  issqf  27330  sqff1o  27376  bposlem7  27484  lgsabs1  27530  gausslemma2dlem1a  27559  lgsquadlem2  27575  addsq2reu  27634  dchrisum0lem1  27710  sltssnb  27992  ltsrec  28024  opphllem6  29063  colhp  29082  lmiinv  29131  lmiopp  29142  wlkeq  30013  eupth2lem3lem3  30611  eupth2lem3lem6  30614  nmounbi  31158  ip2eqi  31238  hvmulcan  31454  hvsubcan2  31457  hi2eq  31487  fh2  32001  riesz4i  32445  cvbr4i  32749  sgnmulsgp  33206  xdivpnfrp  33282  qusker  33693  ellspds  33707  ply1moneq  33902  ballotlemfc0  34907  ballotlemfcc  34908  subfacp1lem5  35689  topfneec2  36900  neibastop3  36906  unccur  38287  cos2h  38295  tan2h  38296  poimirlem25  38329  poimirlem27  38331  dvasin  38388  caures  38444  ismtyima  38487  isdmn3  38758  dmecd  38992  releldmqscoss  39427  tendospcanN  41830  dochsncom  42189  quadfac  43005  sqrtcval  44400  or3or  44782  neicvgel1  44878  rusbcALT  45181  sbcoreleleqVD  45600  climreeq  46362  coseq0  46611  modmkpkne  48137  isidom3  49143  affinecomb1  49515  eenglngeehlnmlem1  49550  2sphere  49562  line2  49565  itscnhlc0yqe  49572  itscnhlc0xyqsol  49578  oduoppcciso  50377