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  4376  fnprb  7237  fntpb  7238  eqfunresadj  7393  eloprabga  7552  ordsucuniel  7859  ordsucun  7860  mpof1o2d  8164  oeoa  8634  ereldm  8799  boxcutc  8997  mapen  9188  mapfien  9427  wemapwe  9725  sdom2en01  10407  prlem936  11159  subcan  11640  mulcan1g  11996  conjmul  12061  ltrec  12226  rebtwnz  13101  xposdif  13419  divelunit  13652  fseq1m1p1  13760  fzm1  13768  fllt  13973  hashfacen  14626  hashf1  14629  ccat0  14748  sgnmulsgn  15291  lenegsq  15517  dvdsmod  16528  bitsmod  16635  smueqlem  16689  rpexp  16927  eulerthlem2  16988  odzdvds  17002  pcelnn  17077  xpsle  17780  isepi  17944  fthmon  18133  cat1  18301  pospropd  18528  grpidpropd  18871  mgmhmpropd  18916  sgrppropd  18949  mndpropd  18980  mhmpropd  19016  grppropd  19191  ghmnsgima  19483  mndodcong  19786  odf1  19806  odf1o1  19816  sylow3lem6  19876  lsmcntzr  19924  efgredlema  19984  cmnpropd  20035  qusecsub  20079  dprdf11  20269  rngpropd  20426  ringpropd  20549  dvdsrpropd  20676  resrhm2b  20884  abvpropd  21122  isorng  21148  lmodprop2d  21229  lsspropd  21322  lmhmpropd  21378  lbspropd  21404  lvecvscan  21419  lvecvscan2  21420  chrnzr  21866  zndvds0  21886  ip2eq  21989  phlpropd  21991  assapropd  22209  qtopcn  24063  tsmsf1o  24494  xmetgt0  24707  txmetcnp  24896  metustsym  24904  nlmmul0or  25032  cnmet  25120  evth  25310  isclmp  25448  minveclem3b  25779  mbfposr  26003  itg2cn  26114  iblcnlem  26139  dvcvx  26370  ulm2  26742  efeq1  26886  dcubic  27204  mcubic  27205  dquart  27211  birthdaylem3  27311  ftalem2  27431  issqf  27493  sqff1o  27539  bposlem7  27647  lgsabs1  27693  gausslemma2dlem1a  27722  lgsquadlem2  27738  addsq2reu  27797  dchrisum0lem1  27873  sltssnb  28185  ltsrec  28217  opphllem6  29258  colhp  29278  lmiinv  29327  lmiopp  29338  wlkeq  30244  eupth2lem3lem3  30861  eupth2lem3lem6  30864  nmounbi  31408  ip2eqi  31488  hvmulcan  31704  hvsubcan2  31707  hi2eq  31737  fh2  32251  riesz4i  32695  cvbr4i  32999  sgnmulsgp  33493  xdivpnfrp  33569  qusker  33980  ellspds  33994  ply1moneq  34190  ballotlemfc0  35195  ballotlemfcc  35196  subfacp1lem5  36116  topfneec2  37322  neibastop3  37328  unccur  38718  cos2h  38726  tan2h  38727  poimirlem25  38755  poimirlem27  38757  dvasin  38814  caures  38886  ismtyima  38929  isdmn3  39200  dmecd  39434  releldmqscoss  39869  tendospcanN  42272  dochsncom  42631  quadfac  43447  sqrtcval  44833  or3or  45215  neicvgel1  45311  rusbcALT  45613  sbcoreleleqVD  46032  climreeq  46830  coseq0  47079  modmkpkne  48642  isidom3  49647  affinecomb1  50019  eenglngeehlnmlem1  50055  2sphere  50066  line2  50069  itscnhlc0yqe  50076  itscnhlc0xyqsol  50082  oduoppcciso  50909