Theorem bitr4id 290

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  baib  535  cad1  1618  necon2abid  2974  reueubd  3367  issetft  3456  reu8  3691  r19.28z  4455  r19.37zv  4460  r19.45zv  4461  r19.44zv  4462  r19.27z  4463  r19.36zv  4465  ralsnsg  4627  eldifvsn  4753  ssunsn2  4783  iunconst  4956  iinconst  4957  iuneqconst  4958  relsng  5750  dmxp  5878  opelres  5944  ordsseleq  6346  ordequn  6422  funssres  6536  fncnv  6565  ffrnbd  6677  fresaun  6705  dff1o5  6783  tz6.12c  6856  funimass4  6898  fndmdifeq0  6989  fneqeql2  6992  unpreima  7008  dffo3  7047  dffo3f  7051  fnnfpeq0  7124  funfvima  7176  f1eqcocnv  7247  fliftf  7261  isocnv3  7278  isomin  7283  eloprabga  7467  mpo2eqb  7490  elpwun  7714  dfom2  7810  opabex3d  7909  opabex3rd  7910  opabex3  7911  f1oweALT  7916  fnwelem  8073  mptsuppd  8129  dfrecs3  8304  oe0m1  8448  oarec  8489  eldifsucnn  8592  naddsuc2  8629  boxcutc  8881  ordunifi  9192  ttrclselem2  9637  r1fin  9687  rankr1c  9735  iscard  9889  iscard2  9890  cardval2  9905  dfac3  10033  kmlem8  10070  xrlenlt  11199  ltxrlt  11205  negcon2  11436  mulne0b  11780  dfinfre  12125  crne0  12140  elznn  12506  zmax  12860  elfznelfzo  13691  modmuladdnn0  13840  hashneq0  14289  xpcogend  14899  sqrtneglem  15191  rexfiuz  15273  rexanuz2  15275  sumsplit  15693  fsum2dlem  15695  odd2np1  16270  divalgb  16333  gcdcllem2  16429  mrcidb2  17543  fncnvimaeqv  18045  qusecsub  19766  domnmuln0  20644  acsfn1p  20734  lbsacsbs  21113  islpir2  21287  islinds2  21770  islbs4  21789  mplcoe1  21994  mplcoe5  21997  mamucl  22347  mavmulcl  22493  mdetunilem8  22565  iscld4  23011  isconn2  23360  kgencn  23502  tx1cn  23555  tx2cn  23556  elmptrab  23773  isfbas  23775  fbfinnfr  23787  cnfcf  23988  fmucndlem  24236  prdsxmslem2  24475  blval2  24508  cnbl0  24719  cnblcld  24720  metcld  25264  ismbf  25587  ismbfcn  25588  itg1val2  25643  itg2split  25708  itg2monolem1  25709  aannenlem1  26294  pilem1  26419  sinq34lt0t  26476  ellogrn  26526  logeftb  26550  gausslemma2dlem1a  27334  sltssnb  27767  bdayle  27914  elznns  28400  zsoring  28407  readdscl  28497  ercgrg  28591  elntg2  29060  usgredgffibi  29399  vtxd0nedgb  29564  vdiscusgrb  29606  upgrspthswlk  29813  s3wwlks2on  30031  sps3wwlks2on  30032  clwwlknonwwlknonb  30183  frgrncvvdeqlem2  30377  ch0pss  31522  h1de2ctlem  31632  adjsym  31910  eigposi  31913  dfadj2  31962  elnlfn  32005  xppreima  32725  1stpreima  32788  2ndpreima  32789  creq0  32817  hashgt1  32890  isunit3  33325  isdrng4  33379  qusxpid  33446  lindflbs  33462  dvdsruassoi  33467  dvdsruasso  33468  dvdsrspss  33470  unitprodclb  33472  lsmsnorb  33474  nsgqusf1olem3  33498  qsfld  33581  esplyind  33733  qtophaus  33995  prsdm  34073  prsrn  34074  1stmbfm  34419  2ndmbfm  34420  eulerpartlemn  34540  reprdifc  34786  circlemeth  34799  bnj1454  35000  bnj984  35110  vonf1owev  35304  dffun10  36108  hfext  36379  isfne4b  36537  neifg  36567  taupilem3  37526  topdifinfindis  37553  topdifinffinlem  37554  finxpsuclem  37604  nlpineqsn  37615  wl-ifp-ncond1  37671  poimirlem23  37846  poimirlem26  37849  cnambfre  37871  0totbnd  37976  opelvvdif  38462  inecmo  38553  brxrn  38581  brin2  38636  suceqsneq  38679  eleccossin  38768  dffunsALTV2  38965  dffunsALTV3  38966  dffunsALTV4  38967  elfunsALTV2  38974  elfunsALTV3  38975  elfunsALTV4  38976  elfunsALTV5  38977  dfdisjs2  38990  eldisjs2  39004  disjres  39025  cvrval2  39556  cvrnbtwn2  39557  cvrnbtwn4  39561  hlateq  39681  islpln5  39817  islvol5  39861  pmap11  40044  4atex  40358  cdleme0ex2N  40506  cdlemefrs29pre00  40677  diaord  41329  dihmeetlem13N  41601  lcfl1  41774  lcfls1N  41817  mapdpglem3  41957  isnacs2  42969  mrefg3  42971  pw2f1ocnv  43300  unielss  43481  onmaxnelsup  43486  onsupnmax  43491  onov0suclim  43537  cantnf2  43588  ordsssucb  43598  relexp0eq  43963  frege124d  44023  uneqsn  44287  k0004lem1  44409  sbcoreleleq  44797  modelac8prim  45254  r19.28zf  45424  climreeq  45880  funressnfv  47310  fmtnorec2lem  47809  sclnbgrelself  48115  gpgiedgdmel  48316  gpgedgel  48317  eenglngeehlnmlem1  49004  eenglngeehlnmlem2  49005  rrx2linest2  49011  itsclinecirc0b  49041  map0cor  49121  ipolublem  49252  ipoglblem  49255  functermc  49774