Theorem bitr4id 292

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 226	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 290	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  baib  543  cad1  1638  necon2abid  3000  reueubd  3385  issetft  3471  reu8  3697  r19.28z  4457  r19.37zv  4462  r19.45zv  4463  r19.44zv  4464  r19.27z  4465  r19.36zv  4467  ralsnsg  4630  eldifvsn  4758  ssunsn2  4786  iunconst  4960  iinconst  4961  iuneqconst  4962  relsng  5775  dmxp  5906  opelres  5972  ordsseleq  6376  ordequn  6452  funssres  6566  fncnv  6595  ffrnbd  6708  fresaun  6736  dff1o5  6817  tz6.12c  6890  funimass4  6932  fndmdifeq0  7026  fneqeql2  7029  unpreima  7045  dffo3  7084  dffo3f  7088  fnnfpeq0  7163  funfvima  7215  f1eqcocnv  7286  fliftf  7300  isocnv3  7317  isomin  7322  eloprabga  7506  mpo2eqb  7529  elpwun  7753  dfom2  7849  opabex3d  7947  opabex3rd  7948  opabex3  7949  f1oweALT  7954  fnwelem  8112  mptsuppd  8168  dfrecs3  8344  oe0m1  8491  oarec  8532  eldifsucnn  8635  naddsuc2  8673  boxcutc  8924  ordunifi  9235  ttrclselem2  9682  r1fin  9732  rankr1c  9780  iscard  9934  iscard2  9935  cardval2  9950  dfac3  10078  kmlem8  10115  xrlenlt  11248  ltxrlt  11254  negcon2  11485  mulne0b  11829  dfinfre  12174  crne0  12189  elznn  12585  zmax  12947  elfznelfzo  13780  modmuladdnn0  13929  hashneq0  14378  xpcogend  14988  sqrtneglem  15294  rexfiuz  15376  rexanuz2  15378  sumsplit  15796  fsum2dlem  15798  odd2np1  16376  divalgb  16439  gcdcllem2  16535  mrcidb2  17651  fncnvimaeqv  18153  qusecsub  19876  domnmuln0  20760  acsfn1p  20849  lbsacsbs  21227  islpir2  21401  islinds2  21866  islbs4  21885  mplcoe1  22091  mplcoe5  22094  mamucl  22462  mavmulcl  22608  mdetunilem8  22680  iscld4  23126  isconn2  23475  kgencn  23617  tx1cn  23670  tx2cn  23671  elmptrab  23888  isfbas  23890  fbfinnfr  23902  cnfcf  24103  fmucndlem  24351  prdsxmslem2  24590  blval2  24623  cnbl0  24834  cnblcld  24835  metcld  25369  ismbf  25691  ismbfcn  25692  itg1val2  25747  itg2split  25812  itg2monolem1  25813  aannenlem1  26393  pilem1  26515  sinq34lt0t  26575  ellogrn  26625  logeftb  26649  gausslemma2dlem1a  27430  sltssnb  27863  bdayle  28010  elznns  28496  zsoring  28503  readdscl  28593  ercgrg  28687  elntg2  29187  usgredgffibi  29526  vtxd0nedgb  29690  vdiscusgrb  29732  upgrspthswlk  29939  s3wwlks2on  30157  sps3wwlks2on  30158  clwwlknonwwlknonb  30309  frgrncvvdeqlem2  30503  ch0pss  31649  h1de2ctlem  31759  adjsym  32037  eigposi  32040  dfadj2  32089  elnlfn  32132  xppreima  32848  1stpreima  32910  2ndpreima  32911  creq0  32939  hashgt1  33011  isunit3  33422  rlocisunit  33458  isdrng4  33483  qusxpid  33550  lindflbs  33566  dvdsruassoi  33571  dvdsruasso  33572  dvdsrspss  33574  unitprodclb  33576  lsmsnorb  33578  nsgqusf1olem3  33602  qsfld  33687  esplyind  33873  qtophaus  34134  prsdm  34212  prsrn  34213  1stmbfm  34558  2ndmbfm  34559  eulerpartlemn  34679  reprdifc  34922  circlemeth  34935  bnj1454  35138  bnj984  35248  vonf1wev  35452  vonf1owevOLD  35454  dffun10  36263  hfext  36534  isfne4b  36702  neifg  36732  taupilem3  37812  topdifinfindis  37841  topdifinffinlem  37842  finxpsuclem  37892  nlpineqsn  37903  wl-ifp-ncond1  37959  poimirlem23  38143  poimirlem26  38146  cnambfre  38168  0totbnd  38273  opelvvdif  38764  inecmo  38855  brxrn  38883  brin2  38938  suceqsneq  38984  eleccossin  39073  dffunsALTV2  39269  dffunsALTV3  39270  dffunsALTV4  39271  elfunsALTV2  39278  elfunsALTV3  39279  elfunsALTV4  39280  elfunsALTV5  39281  dfdisjs2  39294  eldisjs2  39320  disjres  39344  cvrval2  39899  cvrnbtwn2  39900  cvrnbtwn4  39904  hlateq  40024  islpln5  40160  islvol5  40204  pmap11  40387  4atex  40701  cdleme0ex2N  40849  cdlemefrs29pre00  41020  diaord  41672  dihmeetlem13N  41944  lcfl1  42117  lcfls1N  42160  mapdpglem3  42300  isnacs2  43288  mrefg3  43290  pw2f1ocnv  43615  unielss  43796  onmaxnelsup  43801  onsupnmax  43806  onov0suclim  43852  cantnf2  43903  ordsssucb  43913  relexp0eq  44278  frege124d  44338  uneqsn  44602  k0004lem1  44724  sbcoreleleq  45112  modelac8prim  45569  r19.28zf  45738  climreeq  46190  funressnfv  47638  2timesltsqm1  47974  fmtnorec2lem  48152  sclnbgrelself  48471  gpgiedgdmel  48672  gpgedgel  48673  eenglngeehlnmlem1  49360  eenglngeehlnmlem2  49361  rrx2linest2  49367  itsclinecirc0b  49397  map0cor  49477  ipolublem  49608  ipoglblem  49611  functermc  50130