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  544  cad1  1644  necon2abid  3006  reueubd  3393  issetft  3479  reu8  3705  r19.28z  4468  r19.37zv  4473  r19.45zv  4474  r19.44zv  4475  r19.27z  4476  r19.36zv  4478  ralsnsg  4641  eldifvsn  4769  ssunsn2  4797  iunconst  4970  iinconst  4971  iuneqconst  4972  relsng  5789  dmxp  5920  opelres  5985  ordsseleq  6391  ordequn  6467  funssres  6581  fncnv  6610  ffrnbd  6722  fresaun  6750  dff1o5  6831  tz6.12c  6904  funimass4  6946  fndmdifeq0  7040  fneqeql2  7043  unpreima  7059  dffo3  7098  dffo3f  7102  fnnfpeq0  7177  funfvima  7229  f1eqcocnv  7300  fliftf  7314  isocnv3  7331  isomin  7336  eloprabga  7520  mpo2eqb  7543  elpwun  7768  dfom2  7864  opabex3d  7962  opabex3rd  7963  opabex3  7964  f1oweALT  7969  fnwelem  8127  mptsuppd  8183  dfrecs3  8359  oe0m1  8506  oarec  8547  eldifsucnn  8650  naddsuc2  8688  boxcutc  8939  ordunifi  9250  ttrclselem2  9695  r1fin  9745  rankr1c  9793  iscard  9961  iscard2  9962  cardval2  9977  dfac3  10105  kmlem8  10141  xrlenlt  11274  ltxrlt  11280  negcon2  11511  mulne0b  11855  dfinfre  12196  crne0  12211  elznn  12607  zmax  12969  elfznelfzo  13802  modmuladdnn0  13951  hashneq0  14400  xpcogend  15011  sqrtneglem  15317  rexfiuz  15399  rexanuz2  15401  sumsplit  15819  fsum2dlem  15821  odd2np1  16399  divalgb  16462  gcdcllem2  16558  mrcidb2  17674  fncnvimaeqv  18176  qusxpid  19251  qusecsub  19905  domnmuln0  20794  acsfn1p  20880  lbsacsbs  21258  islpir2  21467  islinds2  21932  islbs4  21951  mplcoe1  22157  mplcoe5  22160  mamucl  22527  mavmulcl  22673  mdetunilem8  22745  iscld4  23191  isconn2  23540  kgencn  23682  tx1cn  23735  tx2cn  23736  elmptrab  23953  isfbas  23955  fbfinnfr  23967  cnfcf  24168  fmucndlem  24416  prdsxmslem2  24655  blval2  24688  cnbl0  24899  cnblcld  24900  metcld  25434  ismbf  25756  ismbfcn  25757  itg1val2  25812  itg2split  25877  itg2monolem1  25878  aannenlem1  26458  pilem1  26580  sinq34lt0t  26640  ellogrn  26690  logeftb  26714  gausslemma2dlem1a  27495  sltssnb  27928  bdayle  28075  elznns  28561  zsoring  28568  readdscl  28658  ercgrg  28752  elntg2  29276  usgredgffibi  29615  vtxd0nedgb  29779  vdiscusgrb  29821  upgrspthswlk  30028  s3wwlks2on  30246  sps3wwlks2on  30247  clwwlknonwwlknonb  30398  frgrncvvdeqlem2  30592  ch0pss  31738  h1de2ctlem  31848  adjsym  32126  eigposi  32129  dfadj2  32178  elnlfn  32221  xppreima  32931  1stpreima  32993  2ndpreima  32994  creq0  33022  hashgt1  33094  isunit3  33501  rlocisunit  33537  isdrng4  33559  lindflbs  33636  dvdsruassoi  33641  dvdsruasso  33642  dvdsrspss  33644  unitprodclb  33646  lsmsnorb  33648  nsgqusf1olem3  33668  qsfld  33725  esplyind  33910  qtophaus  34171  prsdm  34249  prsrn  34250  1stmbfm  34595  2ndmbfm  34596  eulerpartlemn  34716  reprdifc  34959  circlemeth  34972  bnj1454  35175  bnj984  35285  vonf1wev  35525  vonf1owevOLD  35527  dffun10  36337  hfext  36608  isfne4b  36775  neifg  36805  taupilem3  37885  topdifinfindis  37914  topdifinffinlem  37915  finxpsuclem  37965  nlpineqsn  37976  wl-ifp-ncond1  38032  poimirlem23  38216  poimirlem26  38219  cnambfre  38241  0totbnd  38346  opelvvdif  38837  inecmo  38928  brxrn  38956  brin2  39011  suceqsneq  39057  eleccossin  39146  dffunsALTV2  39342  dffunsALTV3  39343  dffunsALTV4  39344  elfunsALTV2  39351  elfunsALTV3  39352  elfunsALTV4  39353  elfunsALTV5  39354  dfdisjs2  39367  eldisjs2  39393  disjres  39417  cvrval2  39972  cvrnbtwn2  39973  cvrnbtwn4  39977  hlateq  40097  islpln5  40233  islvol5  40277  pmap11  40460  4atex  40774  cdleme0ex2N  40922  cdlemefrs29pre00  41093  diaord  41745  dihmeetlem13N  42017  lcfl1  42190  lcfls1N  42233  mapdpglem3  42373  isnacs2  43363  mrefg3  43365  pw2f1ocnv  43690  unielss  43871  onmaxnelsup  43876  onsupnmax  43881  onov0suclim  43927  cantnf2  43978  ordsssucb  43988  relexp0eq  44353  frege124d  44413  uneqsn  44677  k0004lem1  44799  sbcoreleleq  45170  modelac8prim  45627  r19.28zf  45803  climreeq  46255  funressnfv  47703  2timesltsqm1  48039  fmtnorec2lem  48217  sclnbgrelself  48536  gpgiedgdmel  48737  gpgedgel  48738  eenglngeehlnmlem1  49436  eenglngeehlnmlem2  49437  rrx2linest2  49443  itsclinecirc0b  49473  map0cor  49552  ipolublem  49683  ipoglblem  49686  functermc  50205