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  4356  fnprb  7154  fntpb  7155  eqfunresadj  7306  eloprabga  7467  ordsucuniel  7766  ordsucun  7767  oeoa  8524  ereldm  8688  boxcutc  8880  mapen  9070  mapfien  9312  wemapwe  9607  sdom2en01  10213  prlem936  10959  subcan  11438  mulcan1g  11792  conjmul  11861  ltrec  12027  rebtwnz  12886  xposdif  13203  divelunit  13436  fseq1m1p1  13542  fzm1  13550  fllt  13754  hashfacen  14405  hashf1  14408  ccat0  14527  lenegsq  15272  dvdsmod  16287  bitsmod  16394  smueqlem  16448  rpexp  16681  eulerthlem2  16741  odzdvds  16755  pcelnn  16830  xpsle  17532  isepi  17696  fthmon  17885  cat1  18053  pospropd  18280  grpidpropd  18619  mgmhmpropd  18655  sgrppropd  18688  mndpropd  18716  mhmpropd  18749  grppropd  18916  ghmnsgima  19204  mndodcong  19506  odf1  19526  odf1o1  19536  sylow3lem6  19596  lsmcntzr  19644  efgredlema  19704  cmnpropd  19755  qusecsub  19799  dprdf11  19989  rngpropd  20144  ringpropd  20258  dvdsrpropd  20385  resrhm2b  20568  abvpropd  20801  isorng  20827  lmodprop2d  20908  lsspropd  21002  lmhmpropd  21058  lbspropd  21084  lvecvscan  21099  lvecvscan2  21100  chrnzr  21518  zndvds0  21538  ip2eq  21641  phlpropd  21643  assapropd  21859  qtopcn  23688  tsmsf1o  24119  xmetgt0  24332  txmetcnp  24521  metustsym  24529  nlmmul0or  24657  cnmet  24745  evth  24935  isclmp  25073  minveclem3b  25404  mbfposr  25628  itg2cn  25739  iblcnlem  25765  dvcvx  25997  ulm2  26365  efeq1  26508  dcubic  26827  mcubic  26828  dquart  26834  birthdaylem3  26934  ftalem2  27055  issqf  27117  sqff1o  27163  bposlem7  27272  lgsabs1  27318  gausslemma2dlem1a  27347  lgsquadlem2  27363  addsq2reu  27422  dchrisum0lem1  27498  sltssnb  27780  ltsrec  27812  opphllem6  28839  colhp  28857  lmiinv  28879  lmiopp  28889  wlkeq  29722  eupth2lem3lem3  30320  eupth2lem3lem6  30323  nmounbi  30867  ip2eqi  30947  hvmulcan  31163  hvsubcan2  31166  hi2eq  31196  fh2  31710  riesz4i  32154  cvbr4i  32458  sgnmulsgn  32935  sgnmulsgp  32936  xdivpnfrp  33012  qusker  33429  ellspds  33448  ply1moneq  33668  ballotlemfc0  34658  ballotlemfcc  34659  subfacp1lem5  35387  topfneec2  36559  neibastop3  36565  unccur  37935  cos2h  37943  tan2h  37944  poimirlem25  37977  poimirlem27  37979  dvasin  38036  caures  38092  ismtyima  38135  isdmn3  38406  dmecd  38642  releldmqscoss  39077  tendospcanN  41480  dochsncom  41839  f1o2d2  42685  sqrtcval  44083  or3or  44465  neicvgel1  44561  rusbcALT  44880  sbcoreleleqVD  45300  climreeq  46058  coseq0  46307  modmkpkne  47812  affinecomb1  49175  eenglngeehlnmlem1  49210  2sphere  49222  line2  49225  itscnhlc0yqe  49232  itscnhlc0xyqsol  49238  oduoppcciso  50038