Theorem bitr4id 289

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  baib  536  cad1  1618  necon2abid  2983  reueubd  3395  reu8  3728  sbc6gOLD  3807  r19.28z  4496  r19.37zv  4500  r19.45zv  4501  r19.44zv  4502  r19.27z  4503  r19.36zv  4505  ralidmOLD  4514  ralsnsg  4671  eldifvsn  4799  ssunsn2  4829  iunconst  5005  iinconst  5006  iuneqconst  5007  relsng  5799  opelres  5985  ordsseleq  6390  ordequn  6464  funssres  6589  fncnv  6618  ffrnbd  6730  fresaun  6759  dff1o5  6839  tz6.12c  6910  funimass4  6953  fndmdifeq0  7042  fneqeql2  7045  unpreima  7061  dffo3  7100  fnnfpeq0  7172  funfvima  7228  f1eqcocnv  7295  f1eqcocnvOLD  7296  fliftf  7308  isocnv3  7325  isomin  7330  eloprabga  7512  eloprabgaOLD  7513  mpo2eqb  7537  elpwun  7752  dfom2  7853  opabex3d  7948  opabex3rd  7949  opabex3  7950  f1oweALT  7955  fnwelem  8113  mptsuppd  8168  dfrecs3  8368  dfrecs3OLD  8369  oe0m1  8517  oarec  8558  eldifsucnn  8659  boxcutc  8931  ordunifi  9289  ttrclselem2  9717  r1fin  9764  rankr1c  9812  iscard  9966  iscard2  9967  cardval2  9982  dfac3  10112  kmlem8  10148  infinf  10557  xrlenlt  11275  ltxrlt  11280  negcon2  11509  mulne0b  11851  dfinfre  12191  crne0  12201  elznn  12570  zmax  12925  elfznelfzo  13733  modmuladdnn0  13876  hashneq0  14320  xpcogend  14917  sqrtneglem  15209  rexfiuz  15290  rexanuz2  15292  sumsplit  15710  fsum2dlem  15712  odd2np1  16280  divalgb  16343  gcdcllem2  16437  mrcidb2  17558  fncnvimaeqv  18067  qusecsub  19697  acsfn1p  20407  lbsacsbs  20761  islpir2  20881  domnmuln0  20906  islinds2  21359  islbs4  21378  mplcoe1  21583  mplcoe5  21586  mamucl  21892  mavmulcl  22040  mdetunilem8  22112  iscld4  22560  isconn2  22909  kgencn  23051  tx1cn  23104  tx2cn  23105  elmptrab  23322  isfbas  23324  fbfinnfr  23336  cnfcf  23537  fmucndlem  23787  prdsxmslem2  24029  blval2  24062  cnbl0  24281  cnblcld  24282  metcld  24814  ismbf  25136  ismbfcn  25137  itg1val2  25192  itg2split  25258  itg2monolem1  25259  aannenlem1  25832  pilem1  25954  sinq34lt0t  26010  ellogrn  26059  logeftb  26083  gausslemma2dlem1a  26857  ercgrg  27757  elntg2  28232  usgredgffibi  28570  vtxd0nedgb  28734  vdiscusgrb  28776  upgrspthswlk  28984  s3wwlks2on  29199  clwwlknonwwlknonb  29348  frgrncvvdeqlem2  29542  ch0pss  30685  h1de2ctlem  30795  adjsym  31073  eigposi  31076  dfadj2  31125  elnlfn  31168  xppreima  31858  1stpreima  31915  2ndpreima  31916  creq0  31947  hashgt1  32007  isdrng4  32383  qusxpid  32463  dvdsruassoi  32477  dvdsruasso  32478  dvdsrspss  32479  lindflbs  32483  lsmsnorb  32489  nsgqusf1olem3  32514  qsfld  32600  qtophaus  32804  prsdm  32882  prsrn  32883  1stmbfm  33247  2ndmbfm  33248  eulerpartlemn  33368  reprdifc  33627  circlemeth  33640  bnj1454  33841  bnj984  33951  dffun10  34874  hfext  35143  isfne4b  35214  neifg  35244  taupilem3  36188  topdifinfindis  36215  topdifinffinlem  36216  finxpsuclem  36266  nlpineqsn  36277  wl-ifp-ncond1  36333  poimirlem23  36499  poimirlem26  36502  cnambfre  36524  0totbnd  36629  suceqsneq  37091  opelvvdif  37115  inecmo  37212  brxrn  37232  brin2  37267  eleccossin  37341  dffunsALTV2  37542  dffunsALTV3  37543  dffunsALTV4  37544  elfunsALTV2  37551  elfunsALTV3  37552  elfunsALTV4  37553  elfunsALTV5  37554  dfdisjs2  37567  eldisjs2  37581  disjres  37602  cvrval2  38132  cvrnbtwn2  38133  cvrnbtwn4  38137  hlateq  38258  islpln5  38394  islvol5  38438  pmap11  38621  4atex  38935  cdleme0ex2N  39083  cdlemefrs29pre00  39254  diaord  39906  dihmeetlem13N  40178  lcfl1  40351  lcfls1N  40394  mapdpglem3  40534  isnacs2  41429  mrefg3  41431  pw2f1ocnv  41761  unielss  41952  onmaxnelsup  41957  onsupnmax  41962  onov0suclim  42009  cantnf2  42060  ordsssucb  42070  naddsuc2  42128  relexp0eq  42437  frege124d  42497  uneqsn  42761  k0004lem1  42883  sbcoreleleq  43281  r19.28zf  43838  dffo3f  43862  climreeq  44315  funressnfv  45739  fmtnorec2lem  46196  eenglngeehlnmlem1  47376  eenglngeehlnmlem2  47377  rrx2linest2  47383  itsclinecirc0b  47413  map0cor  47474  ipolublem  47564  ipoglblem  47567