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  4373  fnprb  7206  fntpb  7207  eqfunresadj  7362  eloprabga  7521  ordsucuniel  7824  ordsucun  7825  mpof1o2d  8126  oeoa  8590  ereldm  8755  boxcutc  8953  mapen  9144  mapfien  9384  wemapwe  9682  sdom2en01  10361  prlem936  11113  subcan  11594  mulcan1g  11950  conjmul  12015  ltrec  12180  rebtwnz  13055  xposdif  13373  divelunit  13606  fseq1m1p1  13713  fzm1  13721  fllt  13926  hashfacen  14579  hashf1  14582  ccat0  14701  sgnmulsgn  15242  lenegsq  15468  dvdsmod  16479  bitsmod  16586  smueqlem  16640  rpexp  16878  eulerthlem2  16939  odzdvds  16953  pcelnn  17028  xpsle  17731  isepi  17895  fthmon  18084  cat1  18252  pospropd  18479  grpidpropd  18822  mgmhmpropd  18867  sgrppropd  18900  mndpropd  18931  mhmpropd  18967  grppropd  19142  ghmnsgima  19434  mndodcong  19736  odf1  19756  odf1o1  19766  sylow3lem6  19826  lsmcntzr  19874  efgredlema  19934  cmnpropd  19985  qusecsub  20029  dprdf11  20219  rngpropd  20376  ringpropd  20499  dvdsrpropd  20626  resrhm2b  20834  abvpropd  21072  isorng  21098  lmodprop2d  21179  lsspropd  21272  lmhmpropd  21328  lbspropd  21354  lvecvscan  21369  lvecvscan2  21370  chrnzr  21816  zndvds0  21836  ip2eq  21939  phlpropd  21941  assapropd  22159  qtopcn  24013  tsmsf1o  24444  xmetgt0  24657  txmetcnp  24846  metustsym  24854  nlmmul0or  24982  cnmet  25070  evth  25260  isclmp  25398  minveclem3b  25729  mbfposr  25953  itg2cn  26064  iblcnlem  26089  dvcvx  26320  ulm2  26694  efeq1  26838  dcubic  27156  mcubic  27157  dquart  27163  birthdaylem3  27263  ftalem2  27383  issqf  27445  sqff1o  27491  bposlem7  27599  lgsabs1  27645  gausslemma2dlem1a  27674  lgsquadlem2  27690  addsq2reu  27749  dchrisum0lem1  27825  sltssnb  28137  ltsrec  28169  opphllem6  29210  colhp  29230  lmiinv  29279  lmiopp  29290  wlkeq  30196  eupth2lem3lem3  30813  eupth2lem3lem6  30816  nmounbi  31360  ip2eqi  31440  hvmulcan  31656  hvsubcan2  31659  hi2eq  31689  fh2  32203  riesz4i  32647  cvbr4i  32951  sgnmulsgp  33405  xdivpnfrp  33481  qusker  33892  ellspds  33906  ply1moneq  34102  ballotlemfc0  35108  ballotlemfcc  35109  subfacp1lem5  35918  topfneec2  37114  neibastop3  37120  unccur  38494  cos2h  38502  tan2h  38503  poimirlem25  38531  poimirlem27  38533  dvasin  38590  caures  38662  ismtyima  38705  isdmn3  38976  dmecd  39210  releldmqscoss  39645  tendospcanN  42048  dochsncom  42407  quadfac  43223  sqrtcval  44600  or3or  44982  neicvgel1  45078  rusbcALT  45381  sbcoreleleqVD  45800  climreeq  46569  coseq0  46818  modmkpkne  48381  isidom3  49386  affinecomb1  49758  eenglngeehlnmlem1  49793  2sphere  49805  line2  49808  itscnhlc0yqe  49815  itscnhlc0xyqsol  49821  oduoppcciso  50618