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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitr3g  313  biass  384  imbibi  391  sbcom2  2174  19.16  2226  19.19  2230  necon1bbid  2965  rspc2gv  3601  reuxfr1d  3724  sbceq1a  3767  sbcg  3829  sbcralt  3838  sbccsb2  4403  csbie2df  4409  reuprg0  4669  disjxun  5108  dmopab2rex  5884  dfres3  5958  xp11  6151  ressn  6261  fnssresb  6643  dmfco  6960  dffo4  7078  f1ompt  7086  funressn  7134  elunirnALT  7229  fliftf  7293  resoprab2  7511  elrnmpores  7530  ralrnmpo  7531  iunpw  7750  ordunisuc2  7823  tfis  7834  tfinds  7839  dfom2  7847  resf1extb  7913  fiun  7924  f1iun  7925  opiota  8041  1stconst  8082  2ndconst  8083  fnsuppeq0  8174  iinon  8312  dfsmo2  8319  oeeui  8569  omabs  8618  naddrid  8650  brecop  8786  ixpsnf1o  8914  boxcutc  8917  ac6sfi  9238  wemapwe  9657  dmttrcl  9681  sdom2en01  10262  ac6num  10439  zorn2lem7  10462  ttukeylem6  10474  alephval2  10532  fpwwe2  10603  fpwwe  10606  nqereu  10889  suplem2pr  11013  map2psrpr  11070  supsrlem  11071  fimaxre3  12136  infm3  12149  crne0  12186  nn1suc  12215  xmulneg1  13236  supxrbnd1  13288  supxrbnd2  13289  iccneg  13440  wrdmap  14518  wrdind  14694  rtrclreclem3  15033  cnpart  15213  sqrt00  15236  lo1resb  15537  o1resb  15539  absefib  16173  efieq1re  16174  sadadd2lem2  16427  saddisjlem  16441  prmind2  16662  isprm7  16685  mreacs  17626  issubc  17804  isfunc  17833  pospo  18311  mndind  18762  eqgval  19116  resscntz  19272  frgpuplem  19709  qusabl  19802  dmdprd  19937  dprdcntz2  19977  dprd2d2  19983  isnzr2  20434  chrdvds  21443  chrcong  21444  znleval  21471  isphld  21570  mpfind  22021  gsummoncoe1  22202  pf1ind  22249  smadiadetr  22569  mp2pm2mplem4  22703  isclo  22981  ist1-2  23241  isnrm2  23252  bwth  23304  nconnsubb  23317  subislly  23375  ptclsg  23509  qtopcld  23607  kqcldsat  23627  qustgplem  24015  tsmssubm  24037  ustuqtop  24141  utop2nei  24145  blval2  24457  caucfil  25190  ioorinv  25484  mbfss  25554  iblss2  25714  dvivthlem1  25920  lhop1  25926  deg1leb  26007  reeff1o  26364  sincosq3sgn  26416  sincosq4sgn  26417  dcubic  26763  efrlim  26886  efrlimOLD  26887  fsumharmonic  26929  isppw  27031  issqf  27053  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  ppiub  27122  lgsdinn0  27263  noetainflem4  27659  eqscut  27724  mulsprop  28040  elzs2  28294  elznns  28297  tglngne  28484  tgelrnln  28564  axlowdimlem14  28889  nbgrssovtx  29295  clwwlknclwwlkdif  29915  eupth2lem2  30155  fusgr2wsp2nb  30270  h2hlm  30916  isch2  31159  ch0pss  31381  nmcfnlbi  31988  jplem1  32204  hatomistici  32298  mdsymlem5  32343  cdjreui  32368  dfimafnf  32567  funcnvmpt  32598  fpwrelmap  32663  nn0min  32752  sgn3da  32766  wrdt2ind  32882  swrdrn3  32884  isarchi  33143  zarcls  33871  ordtconnlem1  33921  esumfsup  34067  esumpcvgval  34075  measvuni  34211  aean  34241  eulerpartlemgh  34376  ballotlemsima  34514  bnj1468  34843  subfacp1lem2a  35174  subfacp1lem6  35179  goeleq12bg  35343  dmopab3rexdif  35399  eldm3  35755  onsuct0  36436  bj-equsexvwd  36776  currysetlem1  36942  bj-restsn  37077  ptrest  37620  ptrecube  37621  poimirlem2  37623  poimirlem23  37644  sdclem2  37743  fdc  37746  fdc1  37747  istotbnd3  37772  sstotbnd  37776  prdstotbnd  37795  rrncmslem  37833  brinxprnres  38286  brcnvrabga  38331  alrmomodm  38348  br1cossxrnres  38446  lub0N  39189  glb0N  39193  cdlemefrs29bpre0  40397  dvhb1dimN  40987  dvhopellsm  41118  dibord  41160  dochnel2  41393  mapdvalc  41630  mapdval4N  41633  diophin  42767  diophun  42768  diophrex  42770  3rexfrabdioph  42792  6rexfrabdioph  42794  7rexfrabdioph  42795  zindbi  42942  tfsconcatrn  43338  rababg  43570  relexpnul  43674  clsk1independent  44042  scottabf  44236  hashnzfzclim  44318  fveqsb  44449  modelac8prim  44989  infxrbnd2  45372  cncfiooicclem1  45898  stoweidlem35  46040  tz6.12-afv  47178  ndmaovg  47189  tz6.12-afv2  47245  ich2exprop  47476  prprspr2  47523  usgrgrtrirex  47953  line2x  48747  line2y  48748  itsclc0b  48765  reuxfr1dd  48799  clddisj  48896  aacllem  49794