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  4378  fnprb  7182  fntpb  7183  eqfunresadj  7335  eloprabga  7498  ordsucuniel  7799  ordsucun  7800  oeoa  8561  ereldm  8724  boxcutc  8914  mapen  9105  mapfien  9359  wemapwe  9650  sdom2en01  10255  prlem936  11000  subcan  11477  mulcan1g  11831  conjmul  11899  ltrec  12065  rebtwnz  12906  xposdif  13222  divelunit  13455  fseq1m1p1  13560  fzm1  13568  fllt  13768  hashfacen  14419  hashf1  14422  ccat0  14541  lenegsq  15287  dvdsmod  16299  bitsmod  16406  smueqlem  16460  rpexp  16692  eulerthlem2  16752  odzdvds  16766  pcelnn  16841  xpsle  17542  isepi  17702  fthmon  17891  cat1  18059  pospropd  18286  grpidpropd  18589  mgmhmpropd  18625  sgrppropd  18658  mndpropd  18686  mhmpropd  18719  grppropd  18883  ghmnsgima  19172  mndodcong  19472  odf1  19492  odf1o1  19502  sylow3lem6  19562  lsmcntzr  19610  efgredlema  19670  cmnpropd  19721  qusecsub  19765  dprdf11  19955  rngpropd  20083  ringpropd  20197  dvdsrpropd  20325  resrhm2b  20511  abvpropd  20744  lmodprop2d  20830  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  lvecvscan  21021  lvecvscan2  21022  chrnzr  21440  zndvds0  21460  ip2eq  21562  phlpropd  21564  assapropd  21781  qtopcn  23601  tsmsf1o  24032  xmetgt0  24246  txmetcnp  24435  metustsym  24443  nlmmul0or  24571  cnmet  24659  evth  24858  isclmp  24997  minveclem3b  25328  mbfposr  25553  itg2cn  25664  iblcnlem  25690  dvcvx  25925  ulm2  26294  efeq1  26437  dcubic  26756  mcubic  26757  dquart  26763  birthdaylem3  26863  ftalem2  26984  issqf  27046  sqff1o  27092  bposlem7  27201  lgsabs1  27247  gausslemma2dlem1a  27276  lgsquadlem2  27292  addsq2reu  27351  dchrisum0lem1  27427  sltrec  27732  opphllem6  28679  colhp  28697  lmiinv  28719  lmiopp  28729  wlkeq  29562  eupth2lem3lem3  30159  eupth2lem3lem6  30162  nmounbi  30705  ip2eqi  30785  hvmulcan  31001  hvsubcan2  31004  hi2eq  31034  fh2  31548  riesz4i  31992  cvbr4i  32296  sgnmulsgn  32767  sgnmulsgp  32768  xdivpnfrp  32853  isorng  33277  qusker  33320  ellspds  33339  ply1moneq  33555  ballotlemfc0  34484  ballotlemfcc  34485  subfacp1lem5  35171  topfneec2  36344  neibastop3  36350  unccur  37597  cos2h  37605  tan2h  37606  poimirlem25  37639  poimirlem27  37641  dvasin  37698  caures  37754  ismtyima  37797  isdmn3  38068  dmecd  38292  releldmqscoss  38652  tendospcanN  41017  dochsncom  41376  f1o2d2  42221  sqrtcval  43630  or3or  44012  neicvgel1  44108  rusbcALT  44428  sbcoreleleqVD  44848  climreeq  45611  coseq0  45862  modmkpkne  47362  affinecomb1  48691  eenglngeehlnmlem1  48726  2sphere  48738  line2  48741  itscnhlc0yqe  48748  itscnhlc0xyqsol  48754  oduoppcciso  49555