Theorem bitr3id 287

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitr3g  315  biass  387  imbibi  394  sbcom2  2196  19.16  2250  19.19  2254  necon1bbid  2986  rspc2gv  3582  reuxfr1d  3703  sbceq1a  3746  sbcg  3807  sbcralt  3816  sbccsb2  4381  csbie2df  4387  reuprg0  4651  disjxun  5088  dmopab2rex  5882  dfres3  5959  xp11  6146  ressn  6257  fnssresb  6628  dmfco  6948  funcnvmpt  6962  dffo4  7069  f1ompt  7077  funressn  7127  elunirnALT  7221  fliftf  7284  resoprab2  7500  elrnmpores  7519  ralrnmpo  7520  iunpw  7739  ordunisuc2  7809  tfis  7820  tfinds  7825  dfom2  7833  resf1extb  7900  fiun  7909  f1iun  7910  opiota  8025  1stconst  8063  2ndconst  8064  fnsuppeq0  8156  iinon  8295  dfsmo2  8302  oeeui  8556  omabs  8605  naddrid  8638  brecop  8776  ixpsnf1o  8905  boxcutc  8908  ac6sfi  9213  wemapwe  9638  dmttrcl  9662  sdom2en01  10245  ac6num  10422  zorn2lem7  10445  ttukeylem6  10457  alephval2  10516  fpwwe2  10587  fpwwe  10590  nqereu  10873  suplem2pr  10997  map2psrpr  11054  supsrlem  11055  fimaxre3  12124  infm3  12137  crne0  12174  nn1suc  12218  xmulneg1  13258  supxrbnd1  13310  supxrbnd2  13311  iccneg  13462  wrdmap  14545  wrdind  14721  rtrclreclem3  15059  cnpart  15239  sqrt00  15262  lo1resb  15563  o1resb  15565  absefib  16202  efieq1re  16203  sadadd2lem2  16456  saddisjlem  16470  prmind2  16691  isprm7  16715  mreacs  17662  issubc  17840  isfunc  17869  pospo  18347  mndind  18834  eqgval  19190  resscntz  19345  frgpuplem  19784  qusabl  19877  dmdprd  20012  dprdcntz2  20052  dprd2d2  20058  isnzr2  20536  chrdvds  21547  chrcong  21548  znleval  21575  isphld  21675  mpfind  22137  gsummoncoe1  22340  pf1ind  22387  smadiadetr  22704  mp2pm2mplem4  22838  isclo  23116  ist1-2  23376  isnrm2  23387  bwth  23439  nconnsubb  23452  subislly  23510  ptclsg  23644  qtopcld  23742  kqcldsat  23762  qustgplem  24150  tsmssubm  24172  ustuqtop  24275  utop2nei  24279  blval2  24591  caucfil  25314  ioorinv  25607  mbfss  25677  iblss2  25837  dvivthlem1  26039  lhop1  26045  deg1leb  26124  reeff1o  26476  sincosq3sgn  26531  sincosq4sgn  26532  dcubic  26877  efrlim  27000  fsumharmonic  27042  isppw  27144  issqf  27166  fsumdvdsmul  27225  ppiub  27234  lgsdinn0  27375  noetainflem4  27770  eqcuts  27844  mulsprop  28189  elzs2  28458  elznns  28461  tglngne  28685  tgelrnln  28765  axlowdimlem14  29091  nbgrssovtx  29497  clwwlknclwwlkdif  30116  eupth2lem2  30356  fusgr2wsp2nb  30471  h2hlm  31118  isch2  31361  ch0pss  31583  nmcfnlbi  32190  jplem1  32406  hatomistici  32500  mdsymlem5  32545  cdjreui  32570  dfimafnf  32777  fpwrelmap  32874  nn0min  32962  sgn3da  32975  wrdt2ind  33081  swrdrn3  33083  gsummptp1  33187  gsummulsubdishift1  33198  isarchi  33312  esplyind  33816  zarcls  34115  ordtconnlem1  34165  esumfsup  34311  esumpcvgval  34319  measvuni  34455  aean  34485  eulerpartlemgh  34619  ballotlemsima  34757  bnj1468  35088  subfacp1lem2a  35468  subfacp1lem6  35473  goeleq12bg  35637  dmopab3rexdif  35693  eldm3  36049  onsuct0  36739  bj-equsexvwd  37186  currysetlem1  37370  bj-restsn  37510  ptrest  38056  ptrecube  38057  poimirlem2  38059  poimirlem23  38080  sdclem2  38179  fdc  38182  fdc1  38183  istotbnd3  38208  sstotbnd  38212  prdstotbnd  38231  rrncmslem  38269  brinxprnres  38734  brcnvrabga  38779  alrmomodm  38796  br1cossxrnres  38975  lub0N  39751  glb0N  39755  cdlemefrs29bpre0  40958  dvhb1dimN  41548  dvhopellsm  41679  dibord  41721  dochnel2  41954  mapdvalc  42191  mapdval4N  42194  diophin  43291  diophun  43292  diophrex  43294  3rexfrabdioph  43312  6rexfrabdioph  43314  7rexfrabdioph  43315  zindbi  43461  tfsconcatrn  43857  rababg  44088  relexpnul  44192  clsk1independent  44560  scottabf  44754  hashnzfzclim  44836  fveqsb  44966  modelac8prim  45506  infxrbnd2  45882  cncfiooicclem1  46405  stoweidlem35  46547  tz6.12-afv  47705  ndmaovg  47716  tz6.12-afv2  47772  ich2exprop  48015  prprspr2  48062  usgrgrtrirex  48510  line2x  49314  line2y  49315  itsclc0b  49332  reuxfr1dd  49366  clddisj  49463  aacllem  50360