Theorem 3bitr3d 310

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 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 280	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sbcne12  4290  fnprb  6844  fntpb  6845  eloprabga  7124  ordsucuniel  7402  ordsucun  7403  oeoa  8080  ereldm  8194  boxcutc  8360  mapen  8535  mapfien  8724  wemapwe  9013  sdom2en01  9577  prlem936  10322  subcan  10795  mulcan1g  11147  conjmul  11211  ltrec  11376  rebtwnz  12200  xposdif  12509  divelunit  12734  fseq1m1p1  12836  fzm1  12841  fllt  13030  hashfacen  13664  hashf1  13667  lenegsq  14518  dvdsmod  15515  bitsmod  15622  smueqlem  15676  rpexp  15897  eulerthlem2  15952  odzdvds  15965  pcelnn  16039  xpsle  16685  isepi  16843  fthmon  17030  pospropd  17577  grpidpropd  17704  mndpropd  17759  mhmpropd  17784  grppropd  17880  ghmnsgima  18127  mndodcong  18405  odf1  18423  odf1o1  18431  sylow3lem6  18491  lsmcntzr  18537  efgredlema  18597  cmnpropd  18646  dprdf11  18866  ringpropd  19026  dvdsrpropd  19140  abvpropd  19307  lmodprop2d  19390  lsspropd  19483  lmhmpropd  19539  lbspropd  19565  lvecvscan  19577  lvecvscan2  19578  assapropd  19793  chrnzr  20363  zndvds0  20383  ip2eq  20483  phlpropd  20485  qtopcn  22010  tsmsf1o  22440  xmetgt0  22655  txmetcnp  22844  metustsym  22852  nlmmul0or  22979  cnmet  23067  evth  23250  isclmp  23388  minveclem3b  23718  mbfposr  23940  itg2cn  24051  iblcnlem  24076  dvcvx  24304  ulm2  24660  efeq1  24798  dcubic  25109  mcubic  25110  dquart  25116  birthdaylem3  25217  ftalem2  25337  issqf  25399  sqff1o  25445  bposlem7  25552  lgsabs1  25598  gausslemma2dlem1a  25627  lgsquadlem2  25643  addsq2reu  25702  dchrisum0lem1  25778  opphllem6  26224  colhp  26242  lmiinv  26264  lmiopp  26274  eupth2lem3lem3  27695  eupth2lem3lem6  27698  nmounbi  28240  ip2eqi  28320  hvmulcan  28536  hvsubcan2  28539  hi2eq  28569  fh2  29083  riesz4i  29527  cvbr4i  29831  xdivpnfrp  30289  isorng  30522  qusker  30568  ellspds  30577  ballotlemfc0  31363  ballotlemfcc  31364  sgnmulsgn  31420  sgnmulsgp  31421  subfacp1lem5  32041  eqfunresadj  32614  sltrec  32889  topfneec2  33315  neibastop3  33321  unccur  34427  cos2h  34435  tan2h  34436  poimirlem25  34469  poimirlem27  34471  dvasin  34530  caures  34588  ismtyima  34634  isdmn3  34905  dmecd  35115  releldmqscoss  35446  tendospcanN  37711  dochsncom  38070  or3or  39877  neicvgel1  39975  rusbcALT  40330  sbcoreleleqVD  40753  climreeq  41457  coseq0  41708  mgmhmpropd  43556  affinecomb1  44192  eenglngeehlnmlem1  44227  2sphere  44239  line2  44242  itscnhlc0yqe  44249  itscnhlc0xyqsol  44255