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 223	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 288	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  535  cad1  1611  necon2abid  2978  reueubd  3390  reu8  3726  sbc6gOLD  3805  r19.28z  4493  r19.37zv  4497  r19.45zv  4498  r19.44zv  4499  r19.27z  4500  r19.36zv  4502  ralidmOLD  4511  ralsnsg  4668  eldifvsn  4796  ssunsn2  4826  iunconst  5000  iinconst  5001  iuneqconst  5002  relsng  5797  opelres  5985  ordsseleq  6392  ordequn  6466  funssres  6591  fncnv  6620  ffrnbd  6732  fresaun  6762  dff1o5  6842  tz6.12c  6913  funimass4  6957  fndmdifeq0  7047  fneqeql2  7050  unpreima  7066  dffo3  7106  dffo3f  7110  fnnfpeq0  7181  funfvima  7236  f1eqcocnv  7304  f1eqcocnvOLD  7305  fliftf  7317  isocnv3  7334  isomin  7339  eloprabga  7522  eloprabgaOLD  7523  mpo2eqb  7547  elpwun  7765  dfom2  7866  opabex3d  7963  opabex3rd  7964  opabex3  7965  f1oweALT  7970  fnwelem  8130  mptsuppd  8185  dfrecs3  8386  dfrecs3OLD  8387  oe0m1  8535  oarec  8576  eldifsucnn  8678  boxcutc  8951  ordunifi  9309  ttrclselem2  9741  r1fin  9788  rankr1c  9836  iscard  9990  iscard2  9991  cardval2  10006  dfac3  10136  kmlem8  10172  infinf  10581  xrlenlt  11301  ltxrlt  11306  negcon2  11535  mulne0b  11877  dfinfre  12217  crne0  12227  elznn  12596  zmax  12951  elfznelfzo  13761  modmuladdnn0  13904  hashneq0  14347  xpcogend  14945  sqrtneglem  15237  rexfiuz  15318  rexanuz2  15320  sumsplit  15738  fsum2dlem  15740  odd2np1  16309  divalgb  16372  gcdcllem2  16466  mrcidb2  17589  fncnvimaeqv  18101  qusecsub  19781  acsfn1p  20676  lbsacsbs  21033  islpir2  21209  domnmuln0  21234  islinds2  21734  islbs4  21753  mplcoe1  21962  mplcoe5  21965  mamucl  22288  mavmulcl  22436  mdetunilem8  22508  iscld4  22956  isconn2  23305  kgencn  23447  tx1cn  23500  tx2cn  23501  elmptrab  23718  isfbas  23720  fbfinnfr  23732  cnfcf  23933  fmucndlem  24183  prdsxmslem2  24425  blval2  24458  cnbl0  24677  cnblcld  24678  metcld  25221  ismbf  25544  ismbfcn  25545  itg1val2  25600  itg2split  25666  itg2monolem1  25667  aannenlem1  26250  pilem1  26375  sinq34lt0t  26431  ellogrn  26480  logeftb  26504  gausslemma2dlem1a  27285  readdscl  28214  ercgrg  28308  elntg2  28783  usgredgffibi  29124  vtxd0nedgb  29289  vdiscusgrb  29331  upgrspthswlk  29539  s3wwlks2on  29754  clwwlknonwwlknonb  29903  frgrncvvdeqlem2  30097  ch0pss  31242  h1de2ctlem  31352  adjsym  31630  eigposi  31633  dfadj2  31682  elnlfn  31725  xppreima  32415  1stpreima  32470  2ndpreima  32471  creq0  32501  hashgt1  32561  isdrng4  32932  qusxpid  33015  dvdsruassoi  33028  dvdsruasso  33029  dvdsrspss  33030  lindflbs  33034  lsmsnorb  33040  nsgqusf1olem3  33065  qsfld  33145  qtophaus  33373  prsdm  33451  prsrn  33452  1stmbfm  33816  2ndmbfm  33817  eulerpartlemn  33937  reprdifc  34195  circlemeth  34208  bnj1454  34409  bnj984  34519  dffun10  35446  hfext  35715  isfne4b  35761  neifg  35791  taupilem3  36734  topdifinfindis  36761  topdifinffinlem  36762  finxpsuclem  36812  nlpineqsn  36823  wl-ifp-ncond1  36879  poimirlem23  37051  poimirlem26  37054  cnambfre  37076  0totbnd  37181  suceqsneq  37642  opelvvdif  37666  inecmo  37763  brxrn  37783  brin2  37818  eleccossin  37892  dffunsALTV2  38093  dffunsALTV3  38094  dffunsALTV4  38095  elfunsALTV2  38102  elfunsALTV3  38103  elfunsALTV4  38104  elfunsALTV5  38105  dfdisjs2  38118  eldisjs2  38132  disjres  38153  cvrval2  38683  cvrnbtwn2  38684  cvrnbtwn4  38688  hlateq  38809  islpln5  38945  islvol5  38989  pmap11  39172  4atex  39486  cdleme0ex2N  39634  cdlemefrs29pre00  39805  diaord  40457  dihmeetlem13N  40729  lcfl1  40902  lcfls1N  40945  mapdpglem3  41085  isnacs2  42048  mrefg3  42050  pw2f1ocnv  42380  unielss  42569  onmaxnelsup  42574  onsupnmax  42579  onov0suclim  42626  cantnf2  42677  ordsssucb  42687  naddsuc2  42745  relexp0eq  43054  frege124d  43114  uneqsn  43378  k0004lem1  43500  sbcoreleleq  43897  r19.28zf  44453  climreeq  44924  funressnfv  46348  fmtnorec2lem  46805  eenglngeehlnmlem1  47733  eenglngeehlnmlem2  47734  rrx2linest2  47740  itsclinecirc0b  47770  map0cor  47830  ipolublem  47920  ipoglblem  47923