Theorem bitr3id 285

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

Hypotheses

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

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 224	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 283	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:  3bitr3g  313  biass  384  imbibi  391  sbcom2  2174  19.16  2226  19.19  2230  necon1bbid  2964  rspc2gv  3589  reuxfr1d  3712  sbceq1a  3755  sbcg  3817  sbcralt  3826  sbccsb2  4390  csbie2df  4396  reuprg0  4656  disjxun  5093  dmopab2rex  5864  dfres3  5939  xp11  6128  ressn  6237  fnssresb  6608  dmfco  6923  dffo4  7041  f1ompt  7049  funressn  7097  elunirnALT  7192  fliftf  7256  resoprab2  7472  elrnmpores  7491  ralrnmpo  7492  iunpw  7711  ordunisuc2  7784  tfis  7795  tfinds  7800  dfom2  7808  resf1extb  7874  fiun  7885  f1iun  7886  opiota  8001  1stconst  8040  2ndconst  8041  fnsuppeq0  8132  iinon  8270  dfsmo2  8277  oeeui  8527  omabs  8576  naddrid  8608  brecop  8744  ixpsnf1o  8872  boxcutc  8875  ac6sfi  9189  wemapwe  9612  dmttrcl  9636  sdom2en01  10215  ac6num  10392  zorn2lem7  10415  ttukeylem6  10427  alephval2  10485  fpwwe2  10556  fpwwe  10559  nqereu  10842  suplem2pr  10966  map2psrpr  11023  supsrlem  11024  fimaxre3  12089  infm3  12102  crne0  12139  nn1suc  12168  xmulneg1  13189  supxrbnd1  13241  supxrbnd2  13242  iccneg  13393  wrdmap  14471  wrdind  14646  rtrclreclem3  14985  cnpart  15165  sqrt00  15188  lo1resb  15489  o1resb  15491  absefib  16125  efieq1re  16126  sadadd2lem2  16379  saddisjlem  16393  prmind2  16614  isprm7  16637  mreacs  17582  issubc  17760  isfunc  17789  pospo  18267  mndind  18720  eqgval  19074  resscntz  19230  frgpuplem  19669  qusabl  19762  dmdprd  19897  dprdcntz2  19937  dprd2d2  19943  isnzr2  20421  chrdvds  21451  chrcong  21452  znleval  21479  isphld  21579  mpfind  22030  gsummoncoe1  22211  pf1ind  22258  smadiadetr  22578  mp2pm2mplem4  22712  isclo  22990  ist1-2  23250  isnrm2  23261  bwth  23313  nconnsubb  23326  subislly  23384  ptclsg  23518  qtopcld  23616  kqcldsat  23636  qustgplem  24024  tsmssubm  24046  ustuqtop  24150  utop2nei  24154  blval2  24466  caucfil  25199  ioorinv  25493  mbfss  25563  iblss2  25723  dvivthlem1  25929  lhop1  25935  deg1leb  26016  reeff1o  26373  sincosq3sgn  26425  sincosq4sgn  26426  dcubic  26772  efrlim  26895  efrlimOLD  26896  fsumharmonic  26938  isppw  27040  issqf  27062  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  ppiub  27131  lgsdinn0  27272  noetainflem4  27668  eqscut  27734  mulsprop  28056  elzs2  28310  elznns  28313  tglngne  28513  tgelrnln  28593  axlowdimlem14  28918  nbgrssovtx  29324  clwwlknclwwlkdif  29941  eupth2lem2  30181  fusgr2wsp2nb  30296  h2hlm  30942  isch2  31185  ch0pss  31407  nmcfnlbi  32014  jplem1  32230  hatomistici  32324  mdsymlem5  32369  cdjreui  32394  dfimafnf  32593  funcnvmpt  32624  fpwrelmap  32689  nn0min  32778  sgn3da  32792  wrdt2ind  32908  swrdrn3  32910  isarchi  33134  zarcls  33840  ordtconnlem1  33890  esumfsup  34036  esumpcvgval  34044  measvuni  34180  aean  34210  eulerpartlemgh  34345  ballotlemsima  34483  bnj1468  34812  subfacp1lem2a  35152  subfacp1lem6  35157  goeleq12bg  35321  dmopab3rexdif  35377  eldm3  35733  onsuct0  36414  bj-equsexvwd  36754  currysetlem1  36920  bj-restsn  37055  ptrest  37598  ptrecube  37599  poimirlem2  37601  poimirlem23  37622  sdclem2  37721  fdc  37724  fdc1  37725  istotbnd3  37750  sstotbnd  37754  prdstotbnd  37773  rrncmslem  37811  brinxprnres  38264  brcnvrabga  38309  alrmomodm  38326  br1cossxrnres  38424  lub0N  39167  glb0N  39171  cdlemefrs29bpre0  40375  dvhb1dimN  40965  dvhopellsm  41096  dibord  41138  dochnel2  41371  mapdvalc  41608  mapdval4N  41611  diophin  42745  diophun  42746  diophrex  42748  3rexfrabdioph  42770  6rexfrabdioph  42772  7rexfrabdioph  42773  zindbi  42919  tfsconcatrn  43315  rababg  43547  relexpnul  43651  clsk1independent  44019  scottabf  44213  hashnzfzclim  44295  fveqsb  44426  modelac8prim  44966  infxrbnd2  45349  cncfiooicclem1  45875  stoweidlem35  46017  tz6.12-afv  47158  ndmaovg  47169  tz6.12-afv2  47225  ich2exprop  47456  prprspr2  47503  usgrgrtrirex  47933  line2x  48727  line2y  48728  itsclc0b  48745  reuxfr1dd  48779  clddisj  48876  aacllem  49774