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  2179  19.16  2233  19.19  2237  necon1bbid  2972  rspc2gv  3587  reuxfr1d  3709  sbceq1a  3752  sbcg  3814  sbcralt  3823  sbccsb2  4390  csbie2df  4396  reuprg0  4660  disjxun  5097  dmopab2rex  5867  dfres3  5944  xp11  6134  ressn  6244  fnssresb  6615  dmfco  6931  funcnvmpt  6944  dffo4  7050  f1ompt  7058  funressn  7107  elunirnALT  7201  fliftf  7264  resoprab2  7480  elrnmpores  7499  ralrnmpo  7500  iunpw  7719  ordunisuc2  7789  tfis  7800  tfinds  7805  dfom2  7813  resf1extb  7879  fiun  7890  f1iun  7891  opiota  8006  1stconst  8045  2ndconst  8046  fnsuppeq0  8137  iinon  8275  dfsmo2  8282  oeeui  8533  omabs  8582  naddrid  8614  brecop  8752  ixpsnf1o  8881  boxcutc  8884  ac6sfi  9189  wemapwe  9611  dmttrcl  9635  sdom2en01  10217  ac6num  10394  zorn2lem7  10417  ttukeylem6  10429  alephval2  10488  fpwwe2  10559  fpwwe  10562  nqereu  10845  suplem2pr  10969  map2psrpr  11026  supsrlem  11027  fimaxre3  12093  infm3  12106  crne0  12143  nn1suc  12172  xmulneg1  13189  supxrbnd1  13241  supxrbnd2  13242  iccneg  13393  wrdmap  14474  wrdind  14650  rtrclreclem3  14988  cnpart  15168  sqrt00  15191  lo1resb  15492  o1resb  15494  absefib  16128  efieq1re  16129  sadadd2lem2  16382  saddisjlem  16396  prmind2  16617  isprm7  16640  mreacs  17586  issubc  17764  isfunc  17793  pospo  18271  mndind  18758  eqgval  19111  resscntz  19267  frgpuplem  19706  qusabl  19799  dmdprd  19934  dprdcntz2  19974  dprd2d2  19980  isnzr2  20456  chrdvds  21486  chrcong  21487  znleval  21514  isphld  21614  mpfind  22075  gsummoncoe1  22257  pf1ind  22304  smadiadetr  22624  mp2pm2mplem4  22758  isclo  23036  ist1-2  23296  isnrm2  23307  bwth  23359  nconnsubb  23372  subislly  23430  ptclsg  23564  qtopcld  23662  kqcldsat  23682  qustgplem  24070  tsmssubm  24092  ustuqtop  24195  utop2nei  24199  blval2  24511  caucfil  25244  ioorinv  25538  mbfss  25608  iblss2  25768  dvivthlem1  25974  lhop1  25980  deg1leb  26061  reeff1o  26418  sincosq3sgn  26470  sincosq4sgn  26471  dcubic  26817  efrlim  26940  efrlimOLD  26941  fsumharmonic  26983  isppw  27085  issqf  27107  fsumdvdsmul  27166  fsumdvdsmulOLD  27168  ppiub  27176  lgsdinn0  27317  noetainflem4  27713  eqcuts  27786  mulsprop  28131  elzs2  28400  elznns  28403  tglngne  28627  tgelrnln  28707  axlowdimlem14  29033  nbgrssovtx  29439  clwwlknclwwlkdif  30059  eupth2lem2  30299  fusgr2wsp2nb  30414  h2hlm  31060  isch2  31303  ch0pss  31525  nmcfnlbi  32132  jplem1  32348  hatomistici  32442  mdsymlem5  32487  cdjreui  32512  dfimafnf  32718  fpwrelmap  32815  nn0min  32904  sgn3da  32918  wrdt2ind  33038  swrdrn3  33040  gsummptp1  33143  gsummulsubdishift1  33154  isarchi  33268  esplyind  33744  zarcls  34044  ordtconnlem1  34094  esumfsup  34240  esumpcvgval  34248  measvuni  34384  aean  34414  eulerpartlemgh  34548  ballotlemsima  34686  bnj1468  35015  subfacp1lem2a  35387  subfacp1lem6  35392  goeleq12bg  35556  dmopab3rexdif  35612  eldm3  35968  onsuct0  36648  bj-equsexvwd  36995  currysetlem1  37161  bj-restsn  37300  ptrest  37833  ptrecube  37834  poimirlem2  37836  poimirlem23  37857  sdclem2  37956  fdc  37959  fdc1  37960  istotbnd3  37985  sstotbnd  37989  prdstotbnd  38008  rrncmslem  38046  brinxprnres  38511  brcnvrabga  38556  alrmomodm  38573  br1cossxrnres  38752  lub0N  39528  glb0N  39532  cdlemefrs29bpre0  40735  dvhb1dimN  41325  dvhopellsm  41456  dibord  41498  dochnel2  41731  mapdvalc  41968  mapdval4N  41971  diophin  43092  diophun  43093  diophrex  43095  3rexfrabdioph  43117  6rexfrabdioph  43119  7rexfrabdioph  43120  zindbi  43266  tfsconcatrn  43662  rababg  43893  relexpnul  43997  clsk1independent  44365  scottabf  44559  hashnzfzclim  44641  fveqsb  44771  modelac8prim  45311  infxrbnd2  45690  cncfiooicclem1  46214  stoweidlem35  46356  tz6.12-afv  47496  ndmaovg  47507  tz6.12-afv2  47563  ich2exprop  47794  prprspr2  47841  usgrgrtrirex  48273  line2x  49077  line2y  49078  itsclc0b  49095  reuxfr1dd  49129  clddisj  49226  aacllem  50123