Theorem bitr4id 294

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr4id.2	⊢ (𝜓 ↔ 𝜒)
bitr4id.1	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4id	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
2		bitr4id.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	bicomi 227	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 292	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  baib  540  cad1  1619  necon2abid  2991  reueubd  3344  reu8  3644  sbc6g  3722  r19.28z  4384  r19.37zv  4388  r19.45zv  4389  r19.44zv  4390  r19.27z  4391  r19.36zv  4393  ralidmOLD  4401  ralsnsg  4558  eldifvsn  4680  ssunsn2  4710  iunconst  4885  iinconst  4886  iuneqconst  4887  relsng  5636  opelres  5822  ordsseleq  6191  ordequn  6262  funssres  6372  fncnv  6401  fresaun  6527  dff1o5  6604  funimass4  6711  fndmdifeq0  6798  fneqeql2  6801  unpreima  6817  dffo3  6852  fnnfpeq0  6924  funfvima  6977  f1eqcocnv  7042  f1eqcocnvOLD  7043  fliftf  7055  isocnv3  7072  isomin  7077  eloprabga  7248  mpo2eqb  7271  elpwun  7483  dfom2  7574  opabex3d  7663  opabex3rd  7664  opabex3  7665  f1oweALT  7670  fnwelem  7823  mptsuppd  7854  dfrecs3  8012  oe0m1  8149  oarec  8191  boxcutc  8516  ordunifi  8786  r1fin  9220  rankr1c  9268  iscard  9422  iscard2  9423  cardval2  9438  dfac3  9566  kmlem8  9602  infinf  10011  xrlenlt  10729  ltxrlt  10734  negcon2  10962  mulne0b  11304  dfinfre  11643  crne0  11652  elznn  12021  zmax  12370  elfznelfzo  13176  modmuladdnn0  13317  hashneq0  13760  xpcogend  14366  sqrtneglem  14659  rexfiuz  14740  rexanuz2  14742  sumsplit  15156  fsum2dlem  15158  odd2np1  15727  divalgb  15790  gcdcllem2  15884  mrcidb2  16932  fncnvimaeqv  17421  acsfn1p  19631  lbsacsbs  19981  islpir2  20077  domnmuln0  20124  islinds2  20563  islbs4  20582  mplcoe1  20782  mplcoe5  20785  mamucl  21086  mavmulcl  21232  mdetunilem8  21304  iscld4  21750  isconn2  22099  kgencn  22241  tx1cn  22294  tx2cn  22295  elmptrab  22512  isfbas  22514  fbfinnfr  22526  cnfcf  22727  fmucndlem  22977  prdsxmslem2  23216  blval2  23249  cnbl0  23460  cnblcld  23461  metcld  23991  ismbf  24313  ismbfcn  24314  itg1val2  24369  itg2split  24434  itg2monolem1  24435  aannenlem1  25008  pilem1  25130  sinq34lt0t  25186  ellogrn  25235  logeftb  25259  gausslemma2dlem1a  26033  ercgrg  26395  elntg2  26863  usgredgffibi  27198  vtxd0nedgb  27362  vdiscusgrb  27404  upgrspthswlk  27611  s3wwlks2on  27826  clwwlknonwwlknonb  27975  frgrncvvdeqlem2  28169  ch0pss  29312  h1de2ctlem  29422  adjsym  29700  eigposi  29703  dfadj2  29752  elnlfn  29795  xppreima  30491  1stpreima  30548  2ndpreima  30549  creq0  30579  hashgt1  30637  qusxpid  31065  lindflbs  31080  lsmsnorb  31085  nsgqusf1olem3  31106  qtophaus  31292  prsdm  31370  prsrn  31371  1stmbfm  31731  2ndmbfm  31732  eulerpartlemn  31852  reprdifc  32111  circlemeth  32124  bnj1454  32327  bnj984  32437  xpord3pred  33338  dffun10  33750  hfext  34019  isfne4b  34064  neifg  34094  taupilem3  34998  topdifinfindis  35028  topdifinffinlem  35029  finxpsuclem  35079  nlpineqsn  35090  wl-ifp-ncond1  35146  wl-dfrabf  35294  poimirlem23  35345  poimirlem26  35348  cnambfre  35370  0totbnd  35476  opelvvdif  35945  inecmo  36034  brxrn  36051  brin2  36082  eleccossin  36148  dffunsALTV2  36342  dffunsALTV3  36343  dffunsALTV4  36344  elfunsALTV2  36351  elfunsALTV3  36352  elfunsALTV4  36353  elfunsALTV5  36354  dfdisjs2  36367  eldisjs2  36381  cvrval2  36835  cvrnbtwn2  36836  cvrnbtwn4  36840  hlateq  36960  islpln5  37096  islvol5  37140  pmap11  37323  4atex  37637  cdleme0ex2N  37785  cdlemefrs29pre00  37956  diaord  38608  dihmeetlem13N  38880  lcfl1  39053  lcfls1N  39096  mapdpglem3  39236  isnacs2  40005  mrefg3  40007  pw2f1ocnv  40336  relexp0eq  40760  frege124d  40820  uneqsn  41084  k0004lem1  41208  sbcoreleleq  41599  dffo3f  42161  climreeq  42606  funressnfv  43986  fmtnorec2lem  44412  eenglngeehlnmlem1  45501  eenglngeehlnmlem2  45502  rrx2linest2  45508  itsclinecirc0b  45538