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  4420  fnprb  7227  fntpb  7228  eqfunresadj  7379  eloprabga  7540  eloprabgaOLD  7541  ordsucuniel  7843  ordsucun  7844  oeoa  8633  ereldm  8793  boxcutc  8979  mapen  9179  mapfien  9445  wemapwe  9734  sdom2en01  10339  prlem936  11084  subcan  11561  mulcan1g  11913  conjmul  11981  ltrec  12147  rebtwnz  12986  xposdif  13300  divelunit  13530  fseq1m1p1  13635  fzm1  13643  fllt  13842  hashfacen  14489  hashf1  14492  ccat0  14610  lenegsq  15355  dvdsmod  16362  bitsmod  16469  smueqlem  16523  rpexp  16755  eulerthlem2  16815  odzdvds  16828  pcelnn  16903  xpsle  17625  isepi  17787  fthmon  17980  cat1  18150  pospropd  18384  grpidpropd  18687  mgmhmpropd  18723  sgrppropd  18756  mndpropd  18784  mhmpropd  18817  grppropd  18981  ghmnsgima  19270  mndodcong  19574  odf1  19594  odf1o1  19604  sylow3lem6  19664  lsmcntzr  19712  efgredlema  19772  cmnpropd  19823  qusecsub  19867  dprdf11  20057  rngpropd  20191  ringpropd  20301  dvdsrpropd  20432  resrhm2b  20618  abvpropd  20852  lmodprop2d  20938  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  lvecvscan  21130  lvecvscan2  21131  chrnzr  21562  zndvds0  21586  ip2eq  21688  phlpropd  21690  assapropd  21909  qtopcn  23737  tsmsf1o  24168  xmetgt0  24383  txmetcnp  24575  metustsym  24583  nlmmul0or  24719  cnmet  24807  evth  25004  isclmp  25143  minveclem3b  25475  mbfposr  25700  itg2cn  25812  iblcnlem  25838  dvcvx  26073  ulm2  26442  efeq1  26584  dcubic  26903  mcubic  26904  dquart  26910  birthdaylem3  27010  ftalem2  27131  issqf  27193  sqff1o  27239  bposlem7  27348  lgsabs1  27394  gausslemma2dlem1a  27423  lgsquadlem2  27439  addsq2reu  27498  dchrisum0lem1  27574  sltrec  27879  opphllem6  28774  colhp  28792  lmiinv  28814  lmiopp  28824  wlkeq  29666  eupth2lem3lem3  30258  eupth2lem3lem6  30261  nmounbi  30804  ip2eqi  30884  hvmulcan  31100  hvsubcan2  31103  hi2eq  31133  fh2  31647  riesz4i  32091  cvbr4i  32395  xdivpnfrp  32899  isorng  33308  qusker  33356  ellspds  33375  ply1moneq  33590  ballotlemfc0  34473  ballotlemfcc  34474  sgnmulsgn  34530  sgnmulsgp  34531  subfacp1lem5  35168  topfneec2  36338  neibastop3  36344  unccur  37589  cos2h  37597  tan2h  37598  poimirlem25  37631  poimirlem27  37633  dvasin  37690  caures  37746  ismtyima  37789  isdmn3  38060  dmecd  38285  releldmqscoss  38641  tendospcanN  41005  dochsncom  41364  f1o2d2  42252  sqrtcval  43630  or3or  44012  neicvgel1  44108  rusbcALT  44434  sbcoreleleqVD  44856  climreeq  45568  coseq0  45819  affinecomb1  48551  eenglngeehlnmlem1  48586  2sphere  48598  line2  48601  itscnhlc0yqe  48608  itscnhlc0xyqsol  48614  oduoppcciso  48881