Theorem bitr3id 284

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	syl5bb 282	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  312  biass  385  sbcom2  2164  19.16  2221  19.19  2225  necon1bbid  2984  rspc2gv  3569  elabgtOLD  3605  reuxfr1d  3688  sbceq1a  3730  sbcg  3799  sbcralt  3809  sbccsb2  4373  csbie2df  4379  reuprg0  4643  disjxun  5076  dmopab2rex  5823  dfres3  5893  xp11  6075  ressn  6185  fnssresb  6550  dmfco  6858  dffo4  6973  f1ompt  6979  funressn  7025  elunirnALT  7119  fliftf  7179  resoprab2  7384  elrnmpores  7402  ralrnmpo  7403  iunpw  7612  ordunisuc2  7679  tfis  7689  tfinds  7694  dfom2  7702  fiun  7772  f1iun  7773  opiota  7885  1stconst  7924  2ndconst  7925  fnsuppeq0  7992  iinon  8155  dfsmo2  8162  oeeui  8409  omabs  8455  brecop  8573  ixpsnf1o  8700  boxcutc  8703  ac6sfi  9019  wemapwe  9416  dmttrcl  9440  sdom2en01  10042  ac6num  10219  zorn2lem7  10242  ttukeylem6  10254  alephval2  10312  fpwwe2  10383  fpwwe  10386  nqereu  10669  suplem2pr  10793  map2psrpr  10850  supsrlem  10851  fimaxre3  11904  infm3  11917  crne0  11949  nn1suc  11978  xmulneg1  12985  supxrbnd1  13037  supxrbnd2  13038  iccneg  13186  wrdmap  14230  wrdind  14416  rtrclreclem3  14752  cnpart  14932  sqrt00  14956  lo1resb  15254  o1resb  15256  absefib  15888  efieq1re  15889  sadadd2lem2  16138  saddisjlem  16152  prmind2  16371  isprm7  16394  mreacs  17348  issubc  17531  isfunc  17560  pospo  18044  mndind  18447  eqgval  18786  resscntz  18919  frgpuplem  19359  qusabl  19447  dmdprd  19582  dprdcntz2  19622  dprd2d2  19628  isnzr2  20515  chrdvds  20713  chrcong  20714  znleval  20743  isphld  20840  mpfind  21298  gsummoncoe1  21456  pf1ind  21502  smadiadetr  21805  mp2pm2mplem4  21939  isclo  22219  ist1-2  22479  isnrm2  22490  bwth  22542  nconnsubb  22555  subislly  22613  ptclsg  22747  qtopcld  22845  kqcldsat  22865  qustgplem  23253  tsmssubm  23275  ustuqtop  23379  utop2nei  23383  blval2  23699  caucfil  24428  ioorinv  24721  mbfss  24791  iblss2  24951  dvivthlem1  25153  lhop1  25159  deg1leb  25241  reeff1o  25587  sincosq3sgn  25638  sincosq4sgn  25639  dcubic  25977  efrlim  26100  fsumharmonic  26142  isppw  26244  issqf  26266  fsumdvdsmul  26325  ppiub  26333  lgsdinn0  26474  tglngne  26892  tgelrnln  26972  axlowdimlem14  27304  nbgrssovtx  27709  clwwlknclwwlkdif  28322  eupth2lem2  28562  fusgr2wsp2nb  28677  h2hlm  29321  isch2  29564  ch0pss  29786  nmcfnlbi  30393  jplem1  30609  hatomistici  30703  mdsymlem5  30748  cdjreui  30773  dfimafnf  30950  funcnvmpt  30983  fpwrelmap  31047  nn0min  31113  wrdt2ind  31204  swrdrn3  31206  isarchi  31415  zarcls  31803  ordtconnlem1  31853  esumfsup  32017  esumpcvgval  32025  measvuni  32161  aean  32191  eulerpartlemgh  32324  ballotlemsima  32461  sgn3da  32487  bnj1468  32805  subfacp1lem2a  33121  subfacp1lem6  33126  goeleq12bg  33290  dmopab3rexdif  33346  eldm3  33707  naddid1  33815  noetainflem4  33922  eqscut  33978  onsuct0  34609  bj-equsexvwd  34942  currysetlem1  35115  bj-restsn  35232  ptrest  35755  ptrecube  35756  poimirlem2  35758  poimirlem23  35779  sdclem2  35879  fdc  35882  fdc1  35883  istotbnd3  35908  sstotbnd  35912  prdstotbnd  35931  rrncmslem  35969  brinxprnres  36405  brcnvrabga  36456  alrmomodm  36470  br1cossxrnres  36545  lub0N  37182  glb0N  37186  cdlemefrs29bpre0  38389  dvhb1dimN  38979  dvhopellsm  39110  dibord  39152  dochnel2  39385  mapdvalc  39622  mapdval4N  39625  diophin  40574  diophun  40575  diophrex  40577  3rexfrabdioph  40599  6rexfrabdioph  40601  7rexfrabdioph  40602  zindbi  40748  rababg  41134  relexpnul  41239  clsk1independent  41609  scottabf  41811  hashnzfzclim  41893  fveqsb  42024  infxrbnd2  42862  cncfiooicclem1  43388  stoweidlem35  43530  tz6.12-afv  44616  ndmaovg  44627  tz6.12-afv2  44683  ich2exprop  44875  prprspr2  44922  line2x  46052  line2y  46053  itsclc0b  46070  clddisj  46149  aacllem  46457