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  2209  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  5895  dfres3  5971  xp11  6162  ressn  6277  fnssresb  6649  dmfco  6969  funcnvmpt  6983  dffo4  7091  f1ompt  7099  funressn  7151  elunirnALT  7244  fliftf  7311  resoprab2  7527  elrnmpores  7546  ralrnmpo  7547  iunpw  7768  ordunisuc2  7838  tfis  7849  tfinds  7854  dfom2  7862  resf1extb  7929  fiun  7938  f1iun  7939  opiota  8053  1stconst  8094  2ndconst  8095  fnsuppeq0  8187  iinon  8326  dfsmo2  8333  oeeui  8589  omabs  8638  naddrid  8671  brecop  8809  ixpsnf1o  8944  boxcutc  8947  ac6sfi  9253  wemapwe  9676  dmttrcl  9700  scottabf  9910  sdom2en01  10351  ac6num  10528  zorn2lem7  10551  ttukeylem6  10563  alephval2  10628  fpwwe2  10699  fpwwe  10702  nqereu  10985  suplem2pr  11109  map2psrpr  11166  supsrlem  11167  fimaxre3  12232  infm3  12245  crne0  12282  nn1suc  12326  xmulneg1  13368  supxrbnd1  13420  supxrbnd2  13421  iccneg  13572  wrdmap  14658  swrdrn3  14769  wrdind  14838  rtrclreclem3  15180  sgn3da  15221  cnpart  15374  sqrt00  15397  lo1resb  15698  o1resb  15700  absefib  16333  efieq1re  16334  sadadd2lem2  16587  saddisjlem  16601  prmind2  16822  isprm7  16846  mreacs  17793  issubc  17971  isfunc  18000  pospo  18478  mndind  18985  eqgval  19350  resscntz  19508  frgpuplem  19947  qusabl  20040  dmdprd  20175  dprdcntz2  20215  dprd2d2  20221  isnzr2  20729  chrdvds  21793  chrcong  21794  znleval  21821  isphld  21921  mpfind  22385  gsummoncoe1  22587  pf1ind  22634  smadiadetr  22951  mp2pm2mplem4  23088  isclo  23366  ist1-2  23626  isnrm2  23637  bwth  23689  nconnsubb  23702  subislly  23761  ptclsg  23895  qtopcld  23993  kqcldsat  24013  qustgplem  24401  tsmssubm  24423  ustuqtop  24526  utop2nei  24530  blval2  24842  caucfil  25565  ioorinv  25858  mbfss  25928  iblss2  26087  dvivthlem1  26289  lhop1  26295  deg1leb  26374  reeff1o  26737  sincosq3sgn  26792  sincosq4sgn  26793  dcubic  27137  efrlim  27260  fsumharmonic  27302  isppw  27404  issqf  27426  fsumdvdsmul  27485  ppiub  27494  lgsdinn0  27635  noetainflem4  28030  eqcuts  28104  mulsprop  28449  elzs2  28718  elznns  28721  tglngne  28946  tgelrnln  29031  tgelrnpln  29187  axlowdimlem14  29466  nbgrssovtx  29875  clwwlknclwwlkdif  30503  eupth2lem2  30753  fusgr2wsp2nb  30868  h2hlm  31515  isch2  31758  ch0pss  31980  nmcfnlbi  32587  jplem1  32803  hatomistici  32897  mdsymlem5  32942  cdjreui  32967  dfimafnf  33163  fpwrelmap  33258  nn0min  33345  wrdt2ind  33449  gsummptp1  33551  gsummulsubdishift1  33562  isarchi  33676  esplyind  34140  zarcls  34439  ordtconnlem1  34489  esumfsup  34635  esumpcvgval  34643  measvuni  34780  aean  34810  eulerpartlemgh  34944  ballotlemsima  35082  bnj1468  35410  subfacp1lem2a  35866  subfacp1lem6  35871  goeleq12bg  36035  dmopab3rexdif  36091  eldm3  36447  onsuct0  37151  bj-equsexvwd  37597  currysetlem1  37782  bj-restsn  37923  ptrest  38457  ptrecube  38458  poimirlem2  38460  poimirlem23  38481  sdclem2  38596  fdc  38599  fdc1  38600  istotbnd3  38625  sstotbnd  38629  prdstotbnd  38648  rrncmslem  38686  brinxprnres  39149  brcnvrabga  39194  alrmomodm  39211  br1cossxrnres  39390  lub0N  40166  glb0N  40170  cdlemefrs29bpre0  41373  dvhb1dimN  41963  dvhopellsm  42094  dibord  42136  dochnel2  42369  mapdvalc  42606  mapdval4N  42609  diophin  43721  diophun  43722  diophrex  43724  3rexfrabdioph  43742  6rexfrabdioph  43744  7rexfrabdioph  43745  zindbi  43891  tfsconcatrn  44287  rababg  44518  relexpnul  44622  clsk1independent  44990  hashnzfzclim  45250  fveqsb  45379  modelac8prim  45919  infxrbnd2  46302  cncfiooicclem1  46825  stoweidlem35  46967  tz6.12-afv  48165  ndmaovg  48176  tz6.12-afv2  48232  ich2exprop  48475  prprspr2  48522  usgrgrtrirex  48970  line2x  49788  line2y  49789  itsclc0b  49806  reuxfr1dd  49839  clddisj  49934  aacllem  50861