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  2972  rspc2gv  3616  reuxfr1d  3738  sbceq1a  3781  sbcg  3843  sbcralt  3852  sbccsb2  4417  csbie2df  4423  reuprg0  4683  disjxun  5122  dmopab2rex  5902  dfres3  5976  xp11  6169  ressn  6279  fnssresb  6665  dmfco  6980  dffo4  7098  f1ompt  7106  funressn  7154  elunirnALT  7249  fliftf  7313  resoprab2  7531  elrnmpores  7550  ralrnmpo  7551  iunpw  7770  ordunisuc2  7844  tfis  7855  tfinds  7860  dfom2  7868  resf1extb  7935  fiun  7946  f1iun  7947  opiota  8063  1stconst  8104  2ndconst  8105  fnsuppeq0  8196  iinon  8359  dfsmo2  8366  oeeui  8619  omabs  8668  naddrid  8700  brecop  8829  ixpsnf1o  8957  boxcutc  8960  ac6sfi  9297  wemapwe  9716  dmttrcl  9740  sdom2en01  10321  ac6num  10498  zorn2lem7  10521  ttukeylem6  10533  alephval2  10591  fpwwe2  10662  fpwwe  10665  nqereu  10948  suplem2pr  11072  map2psrpr  11129  supsrlem  11130  fimaxre3  12193  infm3  12206  crne0  12238  nn1suc  12267  xmulneg1  13290  supxrbnd1  13342  supxrbnd2  13343  iccneg  13494  wrdmap  14569  wrdind  14745  rtrclreclem3  15084  cnpart  15264  sqrt00  15287  lo1resb  15585  o1resb  15587  absefib  16221  efieq1re  16222  sadadd2lem2  16474  saddisjlem  16488  prmind2  16709  isprm7  16732  mreacs  17675  issubc  17853  isfunc  17882  pospo  18360  mndind  18811  eqgval  19165  resscntz  19321  frgpuplem  19758  qusabl  19851  dmdprd  19986  dprdcntz2  20026  dprd2d2  20032  isnzr2  20483  chrdvds  21492  chrcong  21493  znleval  21520  isphld  21619  mpfind  22070  gsummoncoe1  22251  pf1ind  22298  smadiadetr  22618  mp2pm2mplem4  22752  isclo  23030  ist1-2  23290  isnrm2  23301  bwth  23353  nconnsubb  23366  subislly  23424  ptclsg  23558  qtopcld  23656  kqcldsat  23676  qustgplem  24064  tsmssubm  24086  ustuqtop  24190  utop2nei  24194  blval2  24506  caucfil  25240  ioorinv  25534  mbfss  25604  iblss2  25764  dvivthlem1  25970  lhop1  25976  deg1leb  26057  reeff1o  26414  sincosq3sgn  26466  sincosq4sgn  26467  dcubic  26813  efrlim  26936  efrlimOLD  26937  fsumharmonic  26979  isppw  27081  issqf  27103  fsumdvdsmul  27162  fsumdvdsmulOLD  27164  ppiub  27172  lgsdinn0  27313  noetainflem4  27709  eqscut  27774  mulsprop  28090  elzs2  28344  elznns  28347  tglngne  28534  tgelrnln  28614  axlowdimlem14  28939  nbgrssovtx  29345  clwwlknclwwlkdif  29965  eupth2lem2  30205  fusgr2wsp2nb  30320  h2hlm  30966  isch2  31209  ch0pss  31431  nmcfnlbi  32038  jplem1  32254  hatomistici  32348  mdsymlem5  32393  cdjreui  32418  dfimafnf  32619  funcnvmpt  32650  fpwrelmap  32715  nn0min  32804  sgn3da  32818  wrdt2ind  32934  swrdrn3  32936  isarchi  33185  zarcls  33910  ordtconnlem1  33960  esumfsup  34106  esumpcvgval  34114  measvuni  34250  aean  34280  eulerpartlemgh  34415  ballotlemsima  34553  bnj1468  34882  subfacp1lem2a  35207  subfacp1lem6  35212  goeleq12bg  35376  dmopab3rexdif  35432  eldm3  35783  onsuct0  36464  bj-equsexvwd  36804  currysetlem1  36970  bj-restsn  37105  ptrest  37648  ptrecube  37649  poimirlem2  37651  poimirlem23  37672  sdclem2  37771  fdc  37774  fdc1  37775  istotbnd3  37800  sstotbnd  37804  prdstotbnd  37823  rrncmslem  37861  brinxprnres  38314  brcnvrabga  38365  alrmomodm  38382  br1cossxrnres  38471  lub0N  39212  glb0N  39216  cdlemefrs29bpre0  40420  dvhb1dimN  41010  dvhopellsm  41141  dibord  41183  dochnel2  41416  mapdvalc  41653  mapdval4N  41656  diophin  42770  diophun  42771  diophrex  42773  3rexfrabdioph  42795  6rexfrabdioph  42797  7rexfrabdioph  42798  zindbi  42945  tfsconcatrn  43341  rababg  43573  relexpnul  43677  clsk1independent  44045  scottabf  44239  hashnzfzclim  44321  fveqsb  44452  modelac8prim  44992  infxrbnd2  45376  cncfiooicclem1  45902  stoweidlem35  46044  tz6.12-afv  47182  ndmaovg  47193  tz6.12-afv2  47249  ich2exprop  47465  prprspr2  47512  usgrgrtrirex  47942  line2x  48714  line2y  48715  itsclc0b  48732  reuxfr1dd  48765  clddisj  48858  aacllem  49645