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  1614  necon2abid  2985  reueubd  3402  issetft  3499  reu8  3749  sbc6gOLD  3829  r19.28z  4517  r19.37zv  4521  r19.45zv  4522  r19.44zv  4523  r19.27z  4524  r19.36zv  4526  ralidmOLD  4535  ralsnsg  4692  eldifvsn  4822  ssunsn2  4852  iunconst  5028  iinconst  5029  iuneqconst  5030  relsng  5824  dmxp  5952  opelres  6014  ordsseleq  6423  ordequn  6497  funssres  6621  fncnv  6650  ffrnbd  6761  fresaun  6791  dff1o5  6870  tz6.12c  6941  funimass4  6985  fndmdifeq0  7075  fneqeql2  7078  unpreima  7094  dffo3  7134  dffo3f  7138  fnnfpeq0  7210  funfvima  7265  f1eqcocnv  7335  fliftf  7348  isocnv3  7365  isomin  7370  eloprabga  7554  eloprabgaOLD  7555  mpo2eqb  7578  elpwun  7800  dfom2  7901  opabex3d  8002  opabex3rd  8003  opabex3  8004  f1oweALT  8009  fnwelem  8168  mptsuppd  8224  dfrecs3  8424  dfrecs3OLD  8425  oe0m1  8573  oarec  8614  eldifsucnn  8716  naddsuc2  8753  boxcutc  8995  ordunifi  9350  ttrclselem2  9791  r1fin  9838  rankr1c  9886  iscard  10040  iscard2  10041  cardval2  10056  dfac3  10186  kmlem8  10223  infinf  10631  xrlenlt  11351  ltxrlt  11356  negcon2  11585  mulne0b  11927  dfinfre  12272  crne0  12282  elznn  12651  zmax  13006  elfznelfzo  13818  modmuladdnn0  13962  hashneq0  14409  xpcogend  15019  sqrtneglem  15311  rexfiuz  15392  rexanuz2  15394  sumsplit  15812  fsum2dlem  15814  odd2np1  16383  divalgb  16446  gcdcllem2  16540  mrcidb2  17671  fncnvimaeqv  18183  qusecsub  19872  domnmuln0  20726  acsfn1p  20817  lbsacsbs  21176  islpir2  21358  islinds2  21851  islbs4  21870  mplcoe1  22072  mplcoe5  22075  mamucl  22419  mavmulcl  22567  mdetunilem8  22639  iscld4  23087  isconn2  23436  kgencn  23578  tx1cn  23631  tx2cn  23632  elmptrab  23849  isfbas  23851  fbfinnfr  23863  cnfcf  24064  fmucndlem  24314  prdsxmslem2  24556  blval2  24589  cnbl0  24808  cnblcld  24809  metcld  25352  ismbf  25675  ismbfcn  25676  itg1val2  25731  itg2split  25797  itg2monolem1  25798  aannenlem1  26380  pilem1  26505  sinq34lt0t  26561  ellogrn  26610  logeftb  26634  gausslemma2dlem1a  27418  elznns  28397  readdscl  28440  ercgrg  28534  elntg2  29009  usgredgffibi  29350  vtxd0nedgb  29515  vdiscusgrb  29557  upgrspthswlk  29765  s3wwlks2on  29980  clwwlknonwwlknonb  30129  frgrncvvdeqlem2  30323  ch0pss  31468  h1de2ctlem  31578  adjsym  31856  eigposi  31859  dfadj2  31908  elnlfn  31951  xppreima  32656  1stpreima  32710  2ndpreima  32711  creq0  32741  hashgt1  32807  isunit3  33213  isdrng4  33256  qusxpid  33348  lindflbs  33364  dvdsruassoi  33369  dvdsruasso  33370  dvdsrspss  33372  unitprodclb  33374  lsmsnorb  33376  nsgqusf1olem3  33400  qsfld  33483  qtophaus  33774  prsdm  33852  prsrn  33853  1stmbfm  34217  2ndmbfm  34218  eulerpartlemn  34338  reprdifc  34596  circlemeth  34609  bnj1454  34810  bnj984  34920  dffun10  35870  hfext  36139  isfne4b  36254  neifg  36284  taupilem3  37233  topdifinfindis  37260  topdifinffinlem  37261  finxpsuclem  37311  nlpineqsn  37322  wl-ifp-ncond1  37378  poimirlem23  37551  poimirlem26  37554  cnambfre  37576  0totbnd  37681  suceqsneq  38140  opelvvdif  38163  inecmo  38259  brxrn  38278  brin2  38313  eleccossin  38387  dffunsALTV2  38588  dffunsALTV3  38589  dffunsALTV4  38590  elfunsALTV2  38597  elfunsALTV3  38598  elfunsALTV4  38599  elfunsALTV5  38600  dfdisjs2  38613  eldisjs2  38627  disjres  38648  cvrval2  39178  cvrnbtwn2  39179  cvrnbtwn4  39183  hlateq  39304  islpln5  39440  islvol5  39484  pmap11  39667  4atex  39981  cdleme0ex2N  40129  cdlemefrs29pre00  40300  diaord  40952  dihmeetlem13N  41224  lcfl1  41397  lcfls1N  41440  mapdpglem3  41580  isnacs2  42599  mrefg3  42601  pw2f1ocnv  42931  unielss  43119  onmaxnelsup  43124  onsupnmax  43129  onov0suclim  43176  cantnf2  43227  ordsssucb  43237  relexp0eq  43603  frege124d  43663  uneqsn  43927  k0004lem1  44049  sbcoreleleq  44446  r19.28zf  44998  climreeq  45468  funressnfv  46892  fmtnorec2lem  47348  sclnbgrelself  47649  eenglngeehlnmlem1  48389  eenglngeehlnmlem2  48390  rrx2linest2  48396  itsclinecirc0b  48426  map0cor  48486  ipolublem  48576  ipoglblem  48579