Theorem bitr4id 293

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 291	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  539  cad1  1618  necon2abid  2993  reueubd  3346  reu8  3647  sbc6g  3726  r19.28z  4391  r19.37zv  4395  r19.45zv  4396  r19.44zv  4397  r19.27z  4398  r19.36zv  4400  ralidmOLD  4408  ralsnsg  4565  eldifvsn  4687  ssunsn2  4717  iunconst  4892  iinconst  4893  iuneqconst  4894  relsng  5643  opelres  5829  ordsseleq  6198  ordequn  6269  funssres  6379  fncnv  6408  fresaun  6534  dff1o5  6611  funimass4  6718  fndmdifeq0  6805  fneqeql2  6808  unpreima  6824  dffo3  6859  fnnfpeq0  6931  funfvima  6984  f1eqcocnv  7049  f1eqcocnvOLD  7050  fliftf  7062  isocnv3  7079  isomin  7084  eloprabga  7255  mpo2eqb  7278  elpwun  7490  dfom2  7581  opabex3d  7670  opabex3rd  7671  opabex3  7672  f1oweALT  7677  fnwelem  7830  mptsuppd  7861  dfrecs3  8019  oe0m1  8156  oarec  8198  boxcutc  8523  ordunifi  8801  r1fin  9235  rankr1c  9283  iscard  9437  iscard2  9438  cardval2  9453  dfac3  9581  kmlem8  9617  infinf  10026  xrlenlt  10744  ltxrlt  10749  negcon2  10977  mulne0b  11319  dfinfre  11658  crne0  11667  elznn  12036  zmax  12385  elfznelfzo  13191  modmuladdnn0  13332  hashneq0  13775  xpcogend  14381  sqrtneglem  14674  rexfiuz  14755  rexanuz2  14757  sumsplit  15171  fsum2dlem  15173  odd2np1  15742  divalgb  15805  gcdcllem2  15899  mrcidb2  16947  fncnvimaeqv  17436  acsfn1p  19646  lbsacsbs  19996  islpir2  20092  domnmuln0  20139  islinds2  20578  islbs4  20597  mplcoe1  20797  mplcoe5  20800  mamucl  21101  mavmulcl  21247  mdetunilem8  21319  iscld4  21765  isconn2  22114  kgencn  22256  tx1cn  22309  tx2cn  22310  elmptrab  22527  isfbas  22529  fbfinnfr  22541  cnfcf  22742  fmucndlem  22992  prdsxmslem2  23231  blval2  23264  cnbl0  23475  cnblcld  23476  metcld  24006  ismbf  24328  ismbfcn  24329  itg1val2  24384  itg2split  24449  itg2monolem1  24450  aannenlem1  25023  pilem1  25145  sinq34lt0t  25201  ellogrn  25250  logeftb  25274  gausslemma2dlem1a  26048  ercgrg  26410  elntg2  26878  usgredgffibi  27213  vtxd0nedgb  27377  vdiscusgrb  27419  upgrspthswlk  27626  s3wwlks2on  27841  clwwlknonwwlknonb  27990  frgrncvvdeqlem2  28184  ch0pss  29327  h1de2ctlem  29437  adjsym  29715  eigposi  29718  dfadj2  29767  elnlfn  29810  xppreima  30506  1stpreima  30563  2ndpreima  30564  creq0  30594  hashgt1  30652  qusxpid  31080  lindflbs  31095  lsmsnorb  31100  nsgqusf1olem3  31121  qtophaus  31307  prsdm  31385  prsrn  31386  1stmbfm  31746  2ndmbfm  31747  eulerpartlemn  31867  reprdifc  32126  circlemeth  32139  bnj1454  32342  bnj984  32452  xpord3pred  33353  dffun10  33765  hfext  34034  isfne4b  34079  neifg  34109  taupilem3  35013  topdifinfindis  35043  topdifinffinlem  35044  finxpsuclem  35094  nlpineqsn  35105  wl-ifp-ncond1  35161  wl-dfrabf  35309  poimirlem23  35360  poimirlem26  35363  cnambfre  35385  0totbnd  35491  opelvvdif  35960  inecmo  36049  brxrn  36066  brin2  36097  eleccossin  36163  dffunsALTV2  36357  dffunsALTV3  36358  dffunsALTV4  36359  elfunsALTV2  36366  elfunsALTV3  36367  elfunsALTV4  36368  elfunsALTV5  36369  dfdisjs2  36382  eldisjs2  36396  cvrval2  36850  cvrnbtwn2  36851  cvrnbtwn4  36855  hlateq  36975  islpln5  37111  islvol5  37155  pmap11  37338  4atex  37652  cdleme0ex2N  37800  cdlemefrs29pre00  37971  diaord  38623  dihmeetlem13N  38895  lcfl1  39068  lcfls1N  39111  mapdpglem3  39251  isnacs2  40020  mrefg3  40022  pw2f1ocnv  40351  relexp0eq  40775  frege124d  40835  uneqsn  41099  k0004lem1  41223  sbcoreleleq  41614  dffo3f  42176  climreeq  42621  funressnfv  44001  fmtnorec2lem  44427  eenglngeehlnmlem1  45516  eenglngeehlnmlem2  45517  rrx2linest2  45523  itsclinecirc0b  45553