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 223	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 283	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:  3bitr3g  313  biass  386  imbibi  393  sbcom2  2162  19.16  2219  19.19  2223  necon1bbid  2981  rspc2gv  3622  elabgtOLD  3664  reuxfr1d  3747  sbceq1a  3789  sbcg  3857  sbcralt  3867  sbccsb2  4435  csbie2df  4441  reuprg0  4707  disjxun  5147  dmopab2rex  5918  dfres3  5987  xp11  6175  ressn  6285  fnssresb  6673  dmfco  6988  dffo4  7105  f1ompt  7111  funressn  7157  elunirnALT  7251  fliftf  7312  resoprab2  7527  elrnmpores  7546  ralrnmpo  7547  iunpw  7758  ordunisuc2  7833  tfis  7844  tfinds  7849  dfom2  7857  fiun  7929  f1iun  7930  opiota  8045  1stconst  8086  2ndconst  8087  fnsuppeq0  8177  iinon  8340  dfsmo2  8347  oeeui  8602  omabs  8650  naddrid  8682  brecop  8804  ixpsnf1o  8932  boxcutc  8935  ac6sfi  9287  wemapwe  9692  dmttrcl  9716  sdom2en01  10297  ac6num  10474  zorn2lem7  10497  ttukeylem6  10509  alephval2  10567  fpwwe2  10638  fpwwe  10641  nqereu  10924  suplem2pr  11048  map2psrpr  11105  supsrlem  11106  fimaxre3  12160  infm3  12173  crne0  12205  nn1suc  12234  xmulneg1  13248  supxrbnd1  13300  supxrbnd2  13301  iccneg  13449  wrdmap  14496  wrdind  14672  rtrclreclem3  15007  cnpart  15187  sqrt00  15210  lo1resb  15508  o1resb  15510  absefib  16141  efieq1re  16142  sadadd2lem2  16391  saddisjlem  16405  prmind2  16622  isprm7  16645  mreacs  17602  issubc  17785  isfunc  17814  pospo  18298  mndind  18709  eqgval  19057  resscntz  19197  frgpuplem  19640  qusabl  19733  dmdprd  19868  dprdcntz2  19908  dprd2d2  19914  isnzr2  20297  df2idl2  20860  chrdvds  21080  chrcong  21081  znleval  21110  isphld  21207  mpfind  21670  gsummoncoe1  21828  pf1ind  21874  smadiadetr  22177  mp2pm2mplem4  22311  isclo  22591  ist1-2  22851  isnrm2  22862  bwth  22914  nconnsubb  22927  subislly  22985  ptclsg  23119  qtopcld  23217  kqcldsat  23237  qustgplem  23625  tsmssubm  23647  ustuqtop  23751  utop2nei  23755  blval2  24071  caucfil  24800  ioorinv  25093  mbfss  25163  iblss2  25323  dvivthlem1  25525  lhop1  25531  deg1leb  25613  reeff1o  25959  sincosq3sgn  26010  sincosq4sgn  26011  dcubic  26351  efrlim  26474  fsumharmonic  26516  isppw  26618  issqf  26640  fsumdvdsmul  26699  ppiub  26707  lgsdinn0  26848  noetainflem4  27243  eqscut  27306  mulsprop  27586  tglngne  27801  tgelrnln  27881  axlowdimlem14  28213  nbgrssovtx  28618  clwwlknclwwlkdif  29232  eupth2lem2  29472  fusgr2wsp2nb  29587  h2hlm  30233  isch2  30476  ch0pss  30698  nmcfnlbi  31305  jplem1  31521  hatomistici  31615  mdsymlem5  31660  cdjreui  31685  dfimafnf  31860  funcnvmpt  31892  fpwrelmap  31958  nn0min  32026  wrdt2ind  32117  swrdrn3  32119  isarchi  32328  zarcls  32854  ordtconnlem1  32904  esumfsup  33068  esumpcvgval  33076  measvuni  33212  aean  33242  eulerpartlemgh  33377  ballotlemsima  33514  sgn3da  33540  bnj1468  33857  subfacp1lem2a  34171  subfacp1lem6  34176  goeleq12bg  34340  dmopab3rexdif  34396  eldm3  34731  onsuct0  35326  bj-equsexvwd  35659  currysetlem1  35828  bj-restsn  35963  ptrest  36487  ptrecube  36488  poimirlem2  36490  poimirlem23  36511  sdclem2  36610  fdc  36613  fdc1  36614  istotbnd3  36639  sstotbnd  36643  prdstotbnd  36662  rrncmslem  36700  brinxprnres  37160  brcnvrabga  37211  alrmomodm  37228  br1cossxrnres  37318  lub0N  38059  glb0N  38063  cdlemefrs29bpre0  39267  dvhb1dimN  39857  dvhopellsm  39988  dibord  40030  dochnel2  40263  mapdvalc  40500  mapdval4N  40503  diophin  41510  diophun  41511  diophrex  41513  3rexfrabdioph  41535  6rexfrabdioph  41537  7rexfrabdioph  41538  zindbi  41685  tfsconcatrn  42092  rababg  42325  relexpnul  42429  clsk1independent  42797  scottabf  42999  hashnzfzclim  43081  fveqsb  43212  infxrbnd2  44079  cncfiooicclem1  44609  stoweidlem35  44751  tz6.12-afv  45881  ndmaovg  45892  tz6.12-afv2  45948  ich2exprop  46139  prprspr2  46186  line2x  47440  line2y  47441  itsclc0b  47458  clddisj  47536  aacllem  47848