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  3723  sbceq1a  3766  sbcg  3828  sbcralt  3837  sbccsb2  4402  csbie2df  4408  reuprg0  4668  disjxun  5107  dmopab2rex  5883  dfres3  5957  xp11  6150  ressn  6260  fnssresb  6642  dmfco  6959  dffo4  7077  f1ompt  7085  funressn  7133  elunirnALT  7228  fliftf  7292  resoprab2  7510  elrnmpores  7529  ralrnmpo  7530  iunpw  7749  ordunisuc2  7822  tfis  7833  tfinds  7838  dfom2  7846  resf1extb  7912  fiun  7923  f1iun  7924  opiota  8040  1stconst  8081  2ndconst  8082  fnsuppeq0  8173  iinon  8311  dfsmo2  8318  oeeui  8568  omabs  8617  naddrid  8649  brecop  8785  ixpsnf1o  8913  boxcutc  8916  ac6sfi  9237  wemapwe  9656  dmttrcl  9680  sdom2en01  10261  ac6num  10438  zorn2lem7  10461  ttukeylem6  10473  alephval2  10531  fpwwe2  10602  fpwwe  10605  nqereu  10888  suplem2pr  11012  map2psrpr  11069  supsrlem  11070  fimaxre3  12135  infm3  12148  crne0  12180  nn1suc  12209  xmulneg1  13235  supxrbnd1  13287  supxrbnd2  13288  iccneg  13439  wrdmap  14517  wrdind  14693  rtrclreclem3  15032  cnpart  15212  sqrt00  15235  lo1resb  15536  o1resb  15538  absefib  16172  efieq1re  16173  sadadd2lem2  16426  saddisjlem  16440  prmind2  16661  isprm7  16684  mreacs  17625  issubc  17803  isfunc  17832  pospo  18310  mndind  18761  eqgval  19115  resscntz  19271  frgpuplem  19708  qusabl  19801  dmdprd  19936  dprdcntz2  19976  dprd2d2  19982  isnzr2  20433  chrdvds  21442  chrcong  21443  znleval  21470  isphld  21569  mpfind  22020  gsummoncoe1  22201  pf1ind  22248  smadiadetr  22568  mp2pm2mplem4  22702  isclo  22980  ist1-2  23240  isnrm2  23251  bwth  23303  nconnsubb  23316  subislly  23374  ptclsg  23508  qtopcld  23606  kqcldsat  23626  qustgplem  24014  tsmssubm  24036  ustuqtop  24140  utop2nei  24144  blval2  24456  caucfil  25189  ioorinv  25483  mbfss  25553  iblss2  25713  dvivthlem1  25919  lhop1  25925  deg1leb  26006  reeff1o  26363  sincosq3sgn  26415  sincosq4sgn  26416  dcubic  26762  efrlim  26885  efrlimOLD  26886  fsumharmonic  26928  isppw  27030  issqf  27052  fsumdvdsmul  27111  fsumdvdsmulOLD  27113  ppiub  27121  lgsdinn0  27262  noetainflem4  27658  eqscut  27723  mulsprop  28039  elzs2  28293  elznns  28296  tglngne  28483  tgelrnln  28563  axlowdimlem14  28888  nbgrssovtx  29294  clwwlknclwwlkdif  29914  eupth2lem2  30154  fusgr2wsp2nb  30269  h2hlm  30915  isch2  31158  ch0pss  31380  nmcfnlbi  31987  jplem1  32203  hatomistici  32297  mdsymlem5  32342  cdjreui  32367  dfimafnf  32566  funcnvmpt  32597  fpwrelmap  32662  nn0min  32751  sgn3da  32765  wrdt2ind  32881  swrdrn3  32883  isarchi  33142  zarcls  33870  ordtconnlem1  33920  esumfsup  34066  esumpcvgval  34074  measvuni  34210  aean  34240  eulerpartlemgh  34375  ballotlemsima  34513  bnj1468  34842  subfacp1lem2a  35167  subfacp1lem6  35172  goeleq12bg  35336  dmopab3rexdif  35392  eldm3  35743  onsuct0  36424  bj-equsexvwd  36764  currysetlem1  36930  bj-restsn  37065  ptrest  37608  ptrecube  37609  poimirlem2  37611  poimirlem23  37632  sdclem2  37731  fdc  37734  fdc1  37735  istotbnd3  37760  sstotbnd  37764  prdstotbnd  37783  rrncmslem  37821  brinxprnres  38274  brcnvrabga  38319  alrmomodm  38336  br1cossxrnres  38434  lub0N  39177  glb0N  39181  cdlemefrs29bpre0  40385  dvhb1dimN  40975  dvhopellsm  41106  dibord  41148  dochnel2  41381  mapdvalc  41618  mapdval4N  41621  diophin  42753  diophun  42754  diophrex  42756  3rexfrabdioph  42778  6rexfrabdioph  42780  7rexfrabdioph  42781  zindbi  42928  tfsconcatrn  43324  rababg  43556  relexpnul  43660  clsk1independent  44028  scottabf  44222  hashnzfzclim  44304  fveqsb  44435  modelac8prim  44975  infxrbnd2  45358  cncfiooicclem1  45884  stoweidlem35  46026  tz6.12-afv  47164  ndmaovg  47175  tz6.12-afv2  47231  ich2exprop  47462  prprspr2  47509  usgrgrtrirex  47939  line2x  48733  line2y  48734  itsclc0b  48751  reuxfr1dd  48785  clddisj  48882  aacllem  49780