Theorem bitr4di 198

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4di.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
bitr4di	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 132	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 196	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr4g  223  bibi2i  227  3bior1fd  1393  3biant1d  1396  equsalh  1778  eueq3dc  3000  sbcel12g  3162  sbceqg  3163  sbcnel12g  3164  reldisj  3576  r19.3rm  3616  eldifpr  3735  eldiftp  3754  rabxp  4810  elrng  4969  iss  5107  eliniseg  5155  fcnvres  5573  dffv3g  5689  funimass4  5750  fndmdif  5808  fneqeql  5811  funimass3  5819  elrnrexdmb  5842  dff4im  5848  fconst4m  5929  elunirn  5966  riota1  6052  riota2df  6054  f1ocnvfv3  6068  eqfnov  6189  caoftrn  6329  suppimacnvfn  6480  suppssrst  6495  suppssrgst  6496  mpoxopovel  6506  rntpos  6522  ordgt0ge1  6702  iinerm  6875  erinxp  6877  qliftfun  6885  mapdm0  6931  elfi2  7300  fifo  7308  2omap  7312  inl11  7399  ctssdccl  7445  isomnimap  7471  ismkvmap  7488  iswomnimap  7500  omniwomnimkv  7501  pr2nelem  7531  indpi  7703  genpdflem  7868  genpdisj  7884  genpassl  7885  genpassu  7886  ltnqpri  7955  ltpopr  7956  ltexprlemm  7961  ltexprlemdisj  7967  ltexprlemloc  7968  ltrennb  8215  letri3  8400  letr  8402  ltneg  8784  leneg  8787  reapltxor  8911  apsym  8928  suprnubex  9277  suprleubex  9278  elnnnn0  9589  fcdmnn0fsupp  9599  zrevaddcl  9678  znnsub  9679  znn0sub  9693  prime  9728  eluz2  9910  eluz2b1  9984  nn01to3  10000  qrevaddcl  10027  xrletri3  10189  xrletr  10193  iccid  10310  elicopnf  10354  fzsplit2  10438  fzsplit3  10441  fzsn  10455  fzpr  10467  uzsplit  10482  fvinim0ffz  10643  lt2sqi  11047  le2sqi  11048  sseqn  11262  hashf1lem1  11268  ccatlcan  11473  ccatrcan  11474  abs00ap  11811  iooinsup  12026  mertenslem2  12286  fprod2dlemstep  12372  gcddiv  12779  algcvgblem  12810  isprm3  12879  dvdsfi  13000  ballotfilemodife  13223  imasmnd2  13742  imasgrp2  13896  issubg  13959  resgrpisgrp  13981  eqgval  14009  imasrng  14238  ring1  14347  imasring  14352  crngunit  14401  lssle0  14692  lssats2  14734  zndvds  14967  znleval  14971  znleval2  14972  eltg2b  15138  discld  15220  opnssneib  15240  restbasg  15252  ssidcn  15294  cnptoprest2  15324  lmss  15330  txrest  15360  txlm  15363  imasnopn  15383  bldisj  15485  xmeter  15520  bl2ioo  15634  limcdifap  15746  issubgr  16481  bj-sseq  16803  nnti  17005  pw1nct  17016