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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbcne12  4372  fnprb  7196  fntpb  7197  eqfunresadj  7348  eloprabga  7509  ordsucuniel  7808  ordsucun  7809  mpof1o2d  8109  oeoa  8571  ereldm  8736  boxcutc  8927  mapen  9117  mapfien  9356  wemapwe  9654  sdom2en01  10274  prlem936  11020  subcan  11501  mulcan1g  11855  conjmul  11923  ltrec  12088  rebtwnz  12962  xposdif  13279  divelunit  13512  fseq1m1p1  13618  fzm1  13626  fllt  13830  hashfacen  14481  hashf1  14484  ccat0  14603  sgnmulsgn  15136  lenegsq  15362  dvdsmod  16377  bitsmod  16484  smueqlem  16538  rpexp  16771  eulerthlem2  16831  odzdvds  16845  pcelnn  16920  xpsle  17623  isepi  17787  fthmon  17976  cat1  18144  pospropd  18371  grpidpropd  18710  mgmhmpropd  18746  sgrppropd  18779  mndpropd  18807  mhmpropd  18840  grppropd  19008  ghmnsgima  19301  mndodcong  19603  odf1  19623  odf1o1  19633  sylow3lem6  19693  lsmcntzr  19741  efgredlema  19801  cmnpropd  19852  qusecsub  19896  dprdf11  20086  rngpropd  20243  ringpropd  20362  dvdsrpropd  20489  resrhm2b  20678  abvpropd  20907  isorng  20933  lmodprop2d  21014  lsspropd  21107  lmhmpropd  21163  lbspropd  21189  lvecvscan  21204  lvecvscan2  21205  chrnzr  21640  zndvds0  21660  ip2eq  21763  phlpropd  21765  assapropd  21981  qtopcn  23832  tsmsf1o  24263  xmetgt0  24476  txmetcnp  24665  metustsym  24673  nlmmul0or  24801  cnmet  24889  evth  25079  isclmp  25217  minveclem3b  25548  mbfposr  25772  itg2cn  25883  iblcnlem  25909  dvcvx  26140  ulm2  26506  efeq1  26651  dcubic  26969  mcubic  26970  dquart  26976  birthdaylem3  27076  ftalem2  27196  issqf  27258  sqff1o  27304  bposlem7  27412  lgsabs1  27458  gausslemma2dlem1a  27487  lgsquadlem2  27503  addsq2reu  27562  dchrisum0lem1  27638  sltssnb  27920  ltsrec  27952  opphllem6  28983  colhp  29001  lmiinv  29044  lmiopp  29054  wlkeq  29892  eupth2lem3lem3  30490  eupth2lem3lem6  30493  nmounbi  31037  ip2eqi  31117  hvmulcan  31333  hvsubcan2  31336  hi2eq  31366  fh2  31880  riesz4i  32324  cvbr4i  32628  sgnmulsgp  33089  xdivpnfrp  33165  qusker  33584  ellspds  33598  ply1moneq  33795  ballotlemfc0  34800  ballotlemfcc  34801  subfacp1lem5  35547  topfneec2  36729  neibastop3  36735  unccur  38114  cos2h  38122  tan2h  38123  poimirlem25  38156  poimirlem27  38158  dvasin  38215  caures  38271  ismtyima  38314  isdmn3  38585  dmecd  38821  releldmqscoss  39256  tendospcanN  41659  dochsncom  42018  sqrtcval  44229  or3or  44611  neicvgel1  44707  rusbcALT  45012  sbcoreleleqVD  45432  climreeq  46187  coseq0  46436  modmkpkne  47959  affinecomb1  49333  eenglngeehlnmlem1  49368  2sphere  49380  line2  49383  itscnhlc0yqe  49390  itscnhlc0xyqsol  49396  oduoppcciso  50195