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  384  imbibi  391  sbcom2  2154  19.16  2211  19.19  2215  necon1bbid  2975  rspc2gv  3617  elabgtOLDOLD  3660  reuxfr1d  3743  sbceq1a  3785  sbcg  3852  sbcralt  3862  sbccsb2  4430  csbie2df  4436  reuprg0  4702  disjxun  5140  dmopab2rex  5914  dfres3  5984  xp11  6173  ressn  6283  fnssresb  6671  dmfco  6988  dffo4  7107  f1ompt  7115  funressn  7162  elunirnALT  7256  fliftf  7317  resoprab2  7533  elrnmpores  7553  ralrnmpo  7554  iunpw  7767  ordunisuc2  7842  tfis  7853  tfinds  7858  dfom2  7866  fiun  7940  f1iun  7941  opiota  8057  1stconst  8099  2ndconst  8100  fnsuppeq0  8190  iinon  8354  dfsmo2  8361  oeeui  8616  omabs  8665  naddrid  8697  brecop  8820  ixpsnf1o  8948  boxcutc  8951  ac6sfi  9303  wemapwe  9712  dmttrcl  9736  sdom2en01  10317  ac6num  10494  zorn2lem7  10517  ttukeylem6  10529  alephval2  10587  fpwwe2  10658  fpwwe  10661  nqereu  10944  suplem2pr  11068  map2psrpr  11125  supsrlem  11126  fimaxre3  12182  infm3  12195  crne0  12227  nn1suc  12256  xmulneg1  13272  supxrbnd1  13324  supxrbnd2  13325  iccneg  13473  wrdmap  14520  wrdind  14696  rtrclreclem3  15031  cnpart  15211  sqrt00  15234  lo1resb  15532  o1resb  15534  absefib  16166  efieq1re  16167  sadadd2lem2  16416  saddisjlem  16430  prmind2  16647  isprm7  16670  mreacs  17629  issubc  17812  isfunc  17841  pospo  18328  mndind  18771  eqgval  19123  resscntz  19275  frgpuplem  19718  qusabl  19811  dmdprd  19946  dprdcntz2  19986  dprd2d2  19992  isnzr2  20446  chrdvds  21443  chrcong  21444  znleval  21475  isphld  21573  mpfind  22040  gsummoncoe1  22214  pf1ind  22261  smadiadetr  22564  mp2pm2mplem4  22698  isclo  22978  ist1-2  23238  isnrm2  23249  bwth  23301  nconnsubb  23314  subislly  23372  ptclsg  23506  qtopcld  23604  kqcldsat  23624  qustgplem  24012  tsmssubm  24034  ustuqtop  24138  utop2nei  24142  blval2  24458  caucfil  25198  ioorinv  25492  mbfss  25562  iblss2  25722  dvivthlem1  25928  lhop1  25934  deg1leb  26018  reeff1o  26371  sincosq3sgn  26422  sincosq4sgn  26423  dcubic  26765  efrlim  26888  efrlimOLD  26889  fsumharmonic  26931  isppw  27033  issqf  27055  fsumdvdsmul  27114  fsumdvdsmulOLD  27116  ppiub  27124  lgsdinn0  27265  noetainflem4  27660  eqscut  27725  mulsprop  28017  tglngne  28341  tgelrnln  28421  axlowdimlem14  28753  nbgrssovtx  29161  clwwlknclwwlkdif  29776  eupth2lem2  30016  fusgr2wsp2nb  30131  h2hlm  30777  isch2  31020  ch0pss  31242  nmcfnlbi  31849  jplem1  32065  hatomistici  32159  mdsymlem5  32204  cdjreui  32229  dfimafnf  32404  funcnvmpt  32436  fpwrelmap  32499  nn0min  32565  wrdt2ind  32656  swrdrn3  32658  isarchi  32868  zarcls  33411  ordtconnlem1  33461  esumfsup  33625  esumpcvgval  33633  measvuni  33769  aean  33799  eulerpartlemgh  33934  ballotlemsima  34071  sgn3da  34097  bnj1468  34413  subfacp1lem2a  34726  subfacp1lem6  34731  goeleq12bg  34895  dmopab3rexdif  34951  eldm3  35291  onsuct0  35861  bj-equsexvwd  36194  currysetlem1  36362  bj-restsn  36497  ptrest  37027  ptrecube  37028  poimirlem2  37030  poimirlem23  37051  sdclem2  37150  fdc  37153  fdc1  37154  istotbnd3  37179  sstotbnd  37183  prdstotbnd  37202  rrncmslem  37240  brinxprnres  37699  brcnvrabga  37750  alrmomodm  37767  br1cossxrnres  37857  lub0N  38598  glb0N  38602  cdlemefrs29bpre0  39806  dvhb1dimN  40396  dvhopellsm  40527  dibord  40569  dochnel2  40802  mapdvalc  41039  mapdval4N  41042  diophin  42114  diophun  42115  diophrex  42117  3rexfrabdioph  42139  6rexfrabdioph  42141  7rexfrabdioph  42142  zindbi  42289  tfsconcatrn  42694  rababg  42927  relexpnul  43031  clsk1independent  43399  scottabf  43600  hashnzfzclim  43682  fveqsb  43813  infxrbnd2  44674  cncfiooicclem1  45204  stoweidlem35  45346  tz6.12-afv  46476  ndmaovg  46487  tz6.12-afv2  46543  ich2exprop  46734  prprspr2  46781  line2x  47750  line2y  47751  itsclc0b  47768  clddisj  47845  aacllem  48157