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	syl5bb 286	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr3g  316  biass  389  sbcom2  2165  19.16  2225  19.19  2229  sbbibOLD  2285  sbal2OLD  2550  necon1bbid  3026  rspc2gv  3580  elabgt  3609  reuxfr1d  3689  sbceq1a  3731  sbcralt  3801  sbccsb2  4342  csbie2df  4348  reuprg0  4598  disjxun  5028  dmopab2rex  5750  dfres3  5823  xp11  5999  ressn  6104  fnssresb  6441  dmfco  6734  dffo4  6846  f1ompt  6852  funressn  6898  elunirnALT  6989  fliftf  7047  resoprab2  7250  elrnmpores  7267  ralrnmpo  7268  iunpw  7473  ordunisuc2  7539  tfis  7549  tfinds  7554  dfom2  7562  fiun  7626  f1iun  7627  opiota  7739  1stconst  7778  2ndconst  7779  fnsuppeq0  7841  iinon  7960  dfsmo2  7967  oeeui  8211  omabs  8257  brecop  8373  ixpsnf1o  8485  boxcutc  8488  ac6sfi  8746  wemapwe  9144  sdom2en01  9713  ac6num  9890  zorn2lem7  9913  ttukeylem6  9925  alephval2  9983  fpwwe2  10054  fpwwe  10057  nqereu  10340  suplem2pr  10464  map2psrpr  10521  supsrlem  10522  fimaxre3  11575  infm3  11587  crne0  11618  nn1suc  11647  xmulneg1  12650  supxrbnd1  12702  supxrbnd2  12703  iccneg  12850  wrdmap  13889  wrdind  14075  rtrclreclem3  14411  cnpart  14591  sqrt00  14615  lo1resb  14913  o1resb  14915  absefib  15543  efieq1re  15544  sadadd2lem2  15789  saddisjlem  15803  prmind2  16019  isprm7  16042  mreacs  16921  issubc  17097  isfunc  17126  pospo  17575  mndind  17984  eqgval  18321  resscntz  18454  frgpuplem  18890  qusabl  18978  dmdprd  19113  dprdcntz2  19153  dprd2d2  19159  isnzr2  20029  chrdvds  20220  chrcong  20221  znleval  20246  isphld  20343  mpfind  20779  gsummoncoe1  20933  pf1ind  20979  smadiadetr  21280  mp2pm2mplem4  21414  isclo  21692  ist1-2  21952  isnrm2  21963  bwth  22015  nconnsubb  22028  subislly  22086  ptclsg  22220  qtopcld  22318  kqcldsat  22338  qustgplem  22726  tsmssubm  22748  ustuqtop  22852  utop2nei  22856  blval2  23169  caucfil  23887  ioorinv  24180  mbfss  24250  iblss2  24409  dvivthlem1  24611  lhop1  24617  deg1leb  24696  reeff1o  25042  sincosq3sgn  25093  sincosq4sgn  25094  dcubic  25432  efrlim  25555  fsumharmonic  25597  isppw  25699  issqf  25721  fsumdvdsmul  25780  ppiub  25788  lgsdinn0  25929  tglngne  26344  tgelrnln  26424  axlowdimlem14  26749  nbgrssovtx  27151  clwwlknclwwlkdif  27764  eupth2lem2  28004  fusgr2wsp2nb  28119  h2hlm  28763  isch2  29006  ch0pss  29228  nmcfnlbi  29835  jplem1  30051  hatomistici  30145  mdsymlem5  30190  cdjreui  30215  dfimafnf  30395  funcnvmpt  30430  fpwrelmap  30495  nn0min  30562  wrdt2ind  30653  swrdrn3  30655  isarchi  30861  zarcls  31227  ordtconnlem1  31277  esumfsup  31439  esumpcvgval  31447  measvuni  31583  aean  31613  eulerpartlemgh  31746  ballotlemsima  31883  sgn3da  31909  bnj1468  32228  subfacp1lem2a  32540  subfacp1lem6  32545  goeleq12bg  32709  dmopab3rexdif  32765  eldm3  33110  onsuct0  33902  currysetlem1  34382  bj-restsn  34497  ptrest  35056  ptrecube  35057  poimirlem2  35059  poimirlem23  35080  sdclem2  35180  fdc  35183  fdc1  35184  istotbnd3  35209  sstotbnd  35213  prdstotbnd  35232  rrncmslem  35270  brinxprnres  35708  brcnvrabga  35759  alrmomodm  35773  br1cossxrnres  35848  lub0N  36485  glb0N  36489  cdlemefrs29bpre0  37692  dvhb1dimN  38282  dvhopellsm  38413  dibord  38455  dochnel2  38688  mapdvalc  38925  mapdval4N  38928  diophin  39713  diophun  39714  diophrex  39716  3rexfrabdioph  39738  6rexfrabdioph  39740  7rexfrabdioph  39741  zindbi  39887  rababg  40273  relexpnul  40379  clsk1independent  40749  scottabf  40948  hashnzfzclim  41026  fveqsb  41157  infxrbnd2  42001  cncfiooicclem1  42535  stoweidlem35  42677  tz6.12-afv  43729  ndmaovg  43740  tz6.12-afv2  43796  ich2exprop  43988  prprspr2  44035  line2x  45168  line2y  45169  itsclc0b  45186  aacllem  45329