Theorem bitr3id 288

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 227	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 286	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr3g  316  biass  388  imbibiOLD  397  sbcom2  2208  19.16  2261  19.19  2265  necon1bbid  2994  rspc2gv  3585  reuxfr1d  3707  sbceq1a  3749  sbcg  3810  sbcralt  3818  sbccsb2  4394  csbie2df  4400  reuprg0  4662  disjxun  5100  dmopab2rex  5898  dfres3  5974  xp11  6166  ressn  6288  fnssresb  6661  dmfco  6981  funcnvmpt  6995  dffo4  7103  f1ompt  7111  funressn  7163  elunirnALT  7256  fliftf  7323  resoprab2  7539  elrnmpores  7558  ralrnmpo  7559  iunpw  7785  ordunisuc2  7855  tfis  7866  tfinds  7871  dfom2  7879  resf1extb  7946  fiun  7955  f1iun  7956  opiota  8070  1stconst  8111  2ndconst  8112  fnsuppeq0  8209  iinon  8348  dfsmo2  8355  oeeui  8611  omabs  8660  naddrid  8693  brecop  8831  ixpsnf1o  8966  boxcutc  8969  ac6sfi  9275  wemapwe  9698  dmttrcl  9722  scottabf  9939  sdom2en01  10380  ac6num  10557  zorn2lem7  10580  ttukeylem6  10592  alephval2  10657  fpwwe2  10728  fpwwe  10731  nqereu  11014  suplem2pr  11138  map2psrpr  11195  supsrlem  11196  fimaxre3  12263  infm3  12276  crne0  12313  nn1suc  12357  xmulneg1  13399  supxrbnd1  13451  supxrbnd2  13452  iccneg  13603  wrdmap  14691  swrdrn3  14802  wrdind  14871  rtrclreclem3  15213  sgn3da  15254  cnpart  15407  sqrt00  15430  lo1resb  15731  o1resb  15733  absefib  16366  efieq1re  16367  sadadd2lem2  16620  saddisjlem  16634  prmind2  16860  isprm7  16884  mreacs  17832  issubc  18010  isfunc  18039  pospo  18517  mndind  19024  eqgval  19389  resscntz  19547  frgpuplem  19986  qusabl  20079  dmdprd  20214  dprdcntz2  20254  dprd2d2  20260  isnzr2  20768  chrdvds  21832  chrcong  21833  znleval  21860  isphld  21960  mpfind  22424  gsummoncoe1  22626  pf1ind  22673  smadiadetr  22990  mp2pm2mplem4  23127  isclo  23405  ist1-2  23665  isnrm2  23676  bwth  23728  nconnsubb  23741  subislly  23800  ptclsg  23934  qtopcld  24032  kqcldsat  24052  qustgplem  24440  tsmssubm  24462  ustuqtop  24565  utop2nei  24569  blval2  24881  caucfil  25604  ioorinv  25897  mbfss  25967  iblss2  26126  dvivthlem1  26328  lhop1  26334  deg1leb  26413  reeff1o  26774  sincosq3sgn  26829  sincosq4sgn  26830  dcubic  27174  efrlim  27297  fsumharmonic  27339  isppw  27441  issqf  27463  fsumdvdsmul  27522  ppiub  27531  lgsdinn0  27672  noetainflem4  28097  eqcuts  28171  mulsprop  28516  elzs2  28785  elznns  28788  tglngne  29013  tgelrnln  29098  tgelrnpln  29254  axlowdimlem14  29533  nbgrssovtx  29942  clwwlknclwwlkdif  30570  eupth2lem2  30820  fusgr2wsp2nb  30935  h2hlm  31582  isch2  31825  ch0pss  32047  nmcfnlbi  32654  jplem1  32870  hatomistici  32964  mdsymlem5  33009  cdjreui  33034  dfimafnf  33272  fpwrelmap  33367  nn0min  33454  wrdt2ind  33558  gsummptp1  33660  gsummulsubdishift1  33671  isarchi  33785  esplyind  34249  zarcls  34548  ordtconnlem1  34598  esumfsup  34744  esumpcvgval  34752  measvuni  34889  aean  34919  eulerpartlemgh  35052  ballotlemsima  35190  bnj1468  35518  subfacp1lem2a  35987  subfacp1lem6  35992  goeleq12bg  36156  dmopab3rexdif  36212  eldm3  36568  onsuct0  37271  bj-equsexvwd  37717  currysetlem1  37902  bj-restsn  38045  ptrest  38580  ptrecube  38581  poimirlem2  38583  poimirlem23  38604  sdclem2  38719  fdc  38722  fdc1  38723  istotbnd3  38748  sstotbnd  38752  prdstotbnd  38771  rrncmslem  38809  brinxprnres  39272  brcnvrabga  39317  alrmomodm  39334  br1cossxrnres  39513  lub0N  40289  glb0N  40293  cdlemefrs29bpre0  41496  dvhb1dimN  42086  dvhopellsm  42217  dibord  42259  dochnel2  42492  mapdvalc  42729  mapdval4N  42732  diophin  43826  diophun  43827  diophrex  43829  3rexfrabdioph  43847  6rexfrabdioph  43849  7rexfrabdioph  43850  zindbi  43996  tfsconcatrn  44387  rababg  44618  relexpnul  44721  clsk1independent  45089  hashnzfzclim  45349  fveqsb  45478  modelac8prim  46025  infxrbnd2  46423  cncfiooicclem1  46946  stoweidlem35  47088  tz6.12-afv  48286  ndmaovg  48297  tz6.12-afv2  48353  ich2exprop  48596  prprspr2  48643  usgrgrtrirex  49091  line2x  49909  line2y  49910  itsclc0b  49927  reuxfr1dd  49960  clddisj  50055  aacllem  50982