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  4372  fnprb  7214  fntpb  7215  eqfunresadj  7370  eloprabga  7529  ordsucuniel  7835  ordsucun  7836  mpof1o2d  8139  oeoa  8609  ereldm  8774  boxcutc  8972  mapen  9163  mapfien  9403  wemapwe  9701  sdom2en01  10383  prlem936  11135  subcan  11616  mulcan1g  11972  conjmul  12037  ltrec  12202  rebtwnz  13077  xposdif  13395  divelunit  13628  fseq1m1p1  13736  fzm1  13744  fllt  13949  hashfacen  14602  hashf1  14605  ccat0  14724  sgnmulsgn  15267  lenegsq  15493  dvdsmod  16504  bitsmod  16611  smueqlem  16665  rpexp  16903  eulerthlem2  16964  odzdvds  16978  pcelnn  17053  xpsle  17756  isepi  17920  fthmon  18109  cat1  18277  pospropd  18504  grpidpropd  18847  mgmhmpropd  18892  sgrppropd  18925  mndpropd  18956  mhmpropd  18992  grppropd  19167  ghmnsgima  19459  mndodcong  19761  odf1  19781  odf1o1  19791  sylow3lem6  19851  lsmcntzr  19899  efgredlema  19959  cmnpropd  20010  qusecsub  20054  dprdf11  20244  rngpropd  20401  ringpropd  20524  dvdsrpropd  20651  resrhm2b  20859  abvpropd  21097  isorng  21123  lmodprop2d  21204  lsspropd  21297  lmhmpropd  21353  lbspropd  21379  lvecvscan  21394  lvecvscan2  21395  chrnzr  21841  zndvds0  21861  ip2eq  21964  phlpropd  21966  assapropd  22184  qtopcn  24038  tsmsf1o  24469  xmetgt0  24682  txmetcnp  24871  metustsym  24879  nlmmul0or  25007  cnmet  25095  evth  25285  isclmp  25423  minveclem3b  25754  mbfposr  25978  itg2cn  26089  iblcnlem  26114  dvcvx  26345  ulm2  26717  efeq1  26861  dcubic  27179  mcubic  27180  dquart  27186  birthdaylem3  27286  ftalem2  27406  issqf  27468  sqff1o  27514  bposlem7  27622  lgsabs1  27668  gausslemma2dlem1a  27697  lgsquadlem2  27713  addsq2reu  27772  dchrisum0lem1  27848  sltssnb  28160  ltsrec  28192  opphllem6  29233  colhp  29253  lmiinv  29302  lmiopp  29313  wlkeq  30219  eupth2lem3lem3  30836  eupth2lem3lem6  30839  nmounbi  31383  ip2eqi  31463  hvmulcan  31679  hvsubcan2  31682  hi2eq  31712  fh2  32226  riesz4i  32670  cvbr4i  32974  sgnmulsgp  33469  xdivpnfrp  33545  qusker  33956  ellspds  33970  ply1moneq  34166  ballotlemfc0  35171  ballotlemfcc  35172  subfacp1lem5  36035  topfneec2  37236  neibastop3  37242  unccur  38619  cos2h  38627  tan2h  38628  poimirlem25  38656  poimirlem27  38658  dvasin  38715  caures  38787  ismtyima  38830  isdmn3  39101  dmecd  39335  releldmqscoss  39770  tendospcanN  42173  dochsncom  42532  quadfac  43348  sqrtcval  44734  or3or  45116  neicvgel1  45212  rusbcALT  45515  sbcoreleleqVD  45934  climreeq  46718  coseq0  46967  modmkpkne  48530  isidom3  49535  affinecomb1  49907  eenglngeehlnmlem1  49943  2sphere  49954  line2  49957  itscnhlc0yqe  49964  itscnhlc0xyqsol  49970  oduoppcciso  50797