Theorem bitr3id 285

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	bitrid 283	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  313  biass  386  imbibi  393  sbcom2  2159  19.16  2216  19.19  2220  necon1bbid  2981  rspc2gv  3574  elabgtOLD  3609  reuxfr1d  3690  sbceq1a  3732  sbcg  3800  sbcralt  3810  sbccsb2  4374  csbie2df  4380  reuprg0  4642  disjxun  5079  dmopab2rex  5839  dfres3  5908  xp11  6093  ressn  6203  fnssresb  6585  dmfco  6896  dffo4  7011  f1ompt  7017  funressn  7063  elunirnALT  7157  fliftf  7218  resoprab2  7425  elrnmpores  7443  ralrnmpo  7444  iunpw  7653  ordunisuc2  7723  tfis  7733  tfinds  7738  dfom2  7746  fiun  7817  f1iun  7818  opiota  7931  1stconst  7972  2ndconst  7973  fnsuppeq0  8039  iinon  8202  dfsmo2  8209  oeeui  8464  omabs  8512  brecop  8630  ixpsnf1o  8757  boxcutc  8760  ac6sfi  9102  wemapwe  9499  dmttrcl  9523  sdom2en01  10104  ac6num  10281  zorn2lem7  10304  ttukeylem6  10316  alephval2  10374  fpwwe2  10445  fpwwe  10448  nqereu  10731  suplem2pr  10855  map2psrpr  10912  supsrlem  10913  fimaxre3  11967  infm3  11980  crne0  12012  nn1suc  12041  xmulneg1  13049  supxrbnd1  13101  supxrbnd2  13102  iccneg  13250  wrdmap  14294  wrdind  14480  rtrclreclem3  14816  cnpart  14996  sqrt00  15020  lo1resb  15318  o1resb  15320  absefib  15952  efieq1re  15953  sadadd2lem2  16202  saddisjlem  16216  prmind2  16435  isprm7  16458  mreacs  17412  issubc  17595  isfunc  17624  pospo  18108  mndind  18511  eqgval  18850  resscntz  18983  frgpuplem  19423  qusabl  19511  dmdprd  19646  dprdcntz2  19686  dprd2d2  19692  isnzr2  20579  chrdvds  20777  chrcong  20778  znleval  20807  isphld  20904  mpfind  21362  gsummoncoe1  21520  pf1ind  21566  smadiadetr  21869  mp2pm2mplem4  22003  isclo  22283  ist1-2  22543  isnrm2  22554  bwth  22606  nconnsubb  22619  subislly  22677  ptclsg  22811  qtopcld  22909  kqcldsat  22929  qustgplem  23317  tsmssubm  23339  ustuqtop  23443  utop2nei  23447  blval2  23763  caucfil  24492  ioorinv  24785  mbfss  24855  iblss2  25015  dvivthlem1  25217  lhop1  25223  deg1leb  25305  reeff1o  25651  sincosq3sgn  25702  sincosq4sgn  25703  dcubic  26041  efrlim  26164  fsumharmonic  26206  isppw  26308  issqf  26330  fsumdvdsmul  26389  ppiub  26397  lgsdinn0  26538  tglngne  26956  tgelrnln  27036  axlowdimlem14  27368  nbgrssovtx  27773  clwwlknclwwlkdif  28388  eupth2lem2  28628  fusgr2wsp2nb  28743  h2hlm  29387  isch2  29630  ch0pss  29852  nmcfnlbi  30459  jplem1  30675  hatomistici  30769  mdsymlem5  30814  cdjreui  30839  dfimafnf  31016  funcnvmpt  31049  fpwrelmap  31113  nn0min  31179  wrdt2ind  31270  swrdrn3  31272  isarchi  31481  zarcls  31869  ordtconnlem1  31919  esumfsup  32083  esumpcvgval  32091  measvuni  32227  aean  32257  eulerpartlemgh  32390  ballotlemsima  32527  sgn3da  32553  bnj1468  32871  subfacp1lem2a  33187  subfacp1lem6  33192  goeleq12bg  33356  dmopab3rexdif  33412  eldm3  33773  naddid1  33881  noetainflem4  33988  eqscut  34044  onsuct0  34675  bj-equsexvwd  35008  currysetlem1  35180  bj-restsn  35297  ptrest  35820  ptrecube  35821  poimirlem2  35823  poimirlem23  35844  sdclem2  35944  fdc  35947  fdc1  35948  istotbnd3  35973  sstotbnd  35977  prdstotbnd  35996  rrncmslem  36034  brinxprnres  36469  brcnvrabga  36519  alrmomodm  36533  br1cossxrnres  36608  lub0N  37245  glb0N  37249  cdlemefrs29bpre0  38452  dvhb1dimN  39042  dvhopellsm  39173  dibord  39215  dochnel2  39448  mapdvalc  39685  mapdval4N  39688  diophin  40631  diophun  40632  diophrex  40634  3rexfrabdioph  40656  6rexfrabdioph  40658  7rexfrabdioph  40659  zindbi  40806  rababg  41219  relexpnul  41324  clsk1independent  41694  scottabf  41896  hashnzfzclim  41978  fveqsb  42109  infxrbnd2  42956  cncfiooicclem1  43483  stoweidlem35  43625  tz6.12-afv  44723  ndmaovg  44734  tz6.12-afv2  44790  ich2exprop  44981  prprspr2  45028  line2x  46158  line2y  46159  itsclc0b  46176  clddisj  46255  aacllem  46563