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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  baib  545  cad1  1649  necon2abid  3001  reueubd  3386  issetft  3470  reu8  3694  r19.28z  4461  r19.37zv  4466  r19.45zv  4467  r19.44zv  4468  r19.27z  4469  r19.36zv  4471  ralsnsg  4631  eldifvsn  4760  ssunsn2  4786  iunconst  4964  iinconst  4965  iuneqconst  4966  relsng  5784  dmxp  5916  opelres  5981  ordsseleq  6399  ordequn  6475  funssres  6593  fncnv  6624  ffrnbd  6736  fresaun  6764  dff1o5  6845  tz6.12c  6918  funimass4  6960  fndmdifeq0  7054  fneqeql2  7057  unpreima  7073  dffo3  7113  dffo3f  7117  fnnfpeq0  7193  funfvima  7246  f1eqcocnv  7319  fliftf  7333  isocnv3  7350  isomin  7355  eloprabga  7539  mpo2eqb  7562  elpwun  7793  dfom2  7889  opabex3d  7987  opabex3rd  7988  opabex3  7989  f1oweALT  7994  fnwelem  8156  mptsuppd  8218  dfrecs3  8394  oe0m1  8543  oarec  8584  eldifsucnn  8687  naddsuc2  8725  boxcutc  8983  ordunifi  9295  ttrclselem2  9740  r1fin  9793  rankr1c  9843  iscard  10069  iscard2  10070  cardval2  10085  dfac3  10213  kmlem8  10249  xrlenlt  11387  ltxrlt  11393  negcon2  11624  mulne0b  11970  dfinfre  12311  crne0  12326  elznn  12722  zmax  13085  elfznelfzo  13921  modmuladdnn0  14071  hashneq0  14521  xpcogend  15142  sqrtneglem  15448  rexfiuz  15530  rexanuz2  15532  sumsplit  15949  fsum2dlem  15951  odd2np1  16526  divalgb  16589  gcdcllem2  16685  mrcidb2  17807  fncnvimaeqv  18309  qusxpid  19410  qusecsub  20064  domnmuln0  20976  isdrng4  21007  acsfn1p  21071  lbsacsbs  21449  isfieldidl2  21556  islpir2  21669  islinds2  22134  islbs4  22153  mplcoe1  22361  mplcoe5  22364  mamucl  22731  mavmulcl  22877  mdetunilem8  22949  iscld4  23398  isconn2  23747  kgencn  23890  tx1cn  23943  tx2cn  23944  elmptrab  24161  isfbas  24163  fbfinnfr  24175  cnfcf  24376  fmucndlem  24624  prdsxmslem2  24863  blval2  24896  cnbl0  25107  cnblcld  25108  metcld  25642  ismbf  25964  ismbfcn  25965  itg1val2  26020  itg2split  26085  itg2monolem1  26086  aannenlem1  26670  pilem1  26793  sinq34lt0t  26853  ellogrn  26902  logeftb  26926  gausslemma2dlem1a  27707  sltssnb  28170  bdayle  28317  elznns  28803  zsoring  28810  readdscl  28900  ercgrg  28995  elntg2  29578  usgredgffibi  29920  vtxd0nedgb  30084  vdiscusgrb  30126  upgrspthswlk  30339  s3wwlks2on  30560  sps3wwlks2on  30561  clwwlknonwwlknonb  30712  frgrncvvdeqlem2  30916  ch0pss  32062  h1de2ctlem  32172  adjsym  32450  eigposi  32453  dfadj2  32502  elnlfn  32545  xppreima  33296  1stpreima  33357  2ndpreima  33358  creq0  33384  hashgt1  33456  isunit3  33857  rlocisunit  33893  lindflbs  33990  dvdsruassoi  33995  dvdsruasso  33996  dvdsrspss  33998  unitprodclb  34000  lsmsnorb  34002  nsgqusf1olem3  34022  qsfld  34078  esplyind  34263  qtophaus  34524  prsdm  34602  prsrn  34603  1stmbfm  34948  2ndmbfm  34949  eulerpartlemn  35069  reprdifc  35312  circlemeth  35325  bnj1454  35528  bnj984  35638  vonf1wev  35993  vonf1owevOLD  35995  dffun10  36806  hfext  37064  isfne4b  37259  neifg  37289  taupilem3  38383  topdifinfindis  38412  topdifinffinlem  38413  finxpsuclem  38463  nlpineqsn  38474  wl-ifp-ncond1  38530  poimirlem23  38704  poimirlem26  38707  cnambfre  38729  0totbnd  38850  opelvvdif  39339  inecmo  39430  brxrn  39458  brin2  39513  suceqsneq  39559  eleccossin  39648  dffunsALTV2  39844  dffunsALTV3  39845  dffunsALTV4  39846  elfunsALTV2  39853  elfunsALTV3  39854  elfunsALTV4  39855  elfunsALTV5  39856  dfdisjs2  39869  eldisjs2  39895  disjres  39919  cvrval2  40474  cvrnbtwn2  40475  cvrnbtwn4  40479  hlateq  40599  islpln5  40735  islvol5  40779  pmap11  40962  4atex  41276  cdleme0ex2N  41424  cdlemefrs29pre00  41595  diaord  42247  dihmeetlem13N  42519  lcfl1  42692  lcfls1N  42735  mapdpglem3  42875  isnacs2  43860  mrefg3  43862  pw2f1ocnv  44187  unielss  44363  onmaxnelsup  44368  onsupnmax  44373  onov0suclim  44419  cantnf2  44470  ordsssucb  44480  relexp0eq  44844  frege124d  44904  uneqsn  45168  k0004lem1  45290  sbcoreleleq  45660  modelac8prim  46124  r19.28zf  46316  climreeq  46767  funressnfv  48255  2timesltsqm1  48591  fmtnorec2lem  48769  sclnbgrelself  49088  gpgiedgdmel  49289  gpgedgel  49290  eenglngeehlnmlem1  49992  eenglngeehlnmlem2  49993  rrx2linest2  49998  itsclinecirc0b  50028  map0cor  50108  ipolublem  50242  ipoglblem  50245  functermc  50785