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  2176  19.16  2228  19.19  2232  necon1bbid  2967  rspc2gv  3582  reuxfr1d  3704  sbceq1a  3747  sbcg  3809  sbcralt  3818  sbccsb2  4386  csbie2df  4392  reuprg0  4654  disjxun  5091  dmopab2rex  5862  dfres3  5938  xp11  6128  ressn  6238  fnssresb  6609  dmfco  6924  dffo4  7042  f1ompt  7050  funressn  7098  elunirnALT  7192  fliftf  7255  resoprab2  7471  elrnmpores  7490  ralrnmpo  7491  iunpw  7710  ordunisuc2  7780  tfis  7791  tfinds  7796  dfom2  7804  resf1extb  7870  fiun  7881  f1iun  7882  opiota  7997  1stconst  8036  2ndconst  8037  fnsuppeq0  8128  iinon  8266  dfsmo2  8273  oeeui  8523  omabs  8572  naddrid  8604  brecop  8740  ixpsnf1o  8868  boxcutc  8871  ac6sfi  9174  wemapwe  9593  dmttrcl  9617  sdom2en01  10199  ac6num  10376  zorn2lem7  10399  ttukeylem6  10411  alephval2  10469  fpwwe2  10540  fpwwe  10543  nqereu  10826  suplem2pr  10950  map2psrpr  11007  supsrlem  11008  fimaxre3  12074  infm3  12087  crne0  12124  nn1suc  12153  xmulneg1  13174  supxrbnd1  13226  supxrbnd2  13227  iccneg  13378  wrdmap  14459  wrdind  14635  rtrclreclem3  14973  cnpart  15153  sqrt00  15176  lo1resb  15477  o1resb  15479  absefib  16113  efieq1re  16114  sadadd2lem2  16367  saddisjlem  16381  prmind2  16602  isprm7  16625  mreacs  17570  issubc  17748  isfunc  17777  pospo  18255  mndind  18742  eqgval  19095  resscntz  19251  frgpuplem  19690  qusabl  19783  dmdprd  19918  dprdcntz2  19958  dprd2d2  19964  isnzr2  20439  chrdvds  21469  chrcong  21470  znleval  21497  isphld  21597  mpfind  22048  gsummoncoe1  22229  pf1ind  22276  smadiadetr  22596  mp2pm2mplem4  22730  isclo  23008  ist1-2  23268  isnrm2  23279  bwth  23331  nconnsubb  23344  subislly  23402  ptclsg  23536  qtopcld  23634  kqcldsat  23654  qustgplem  24042  tsmssubm  24064  ustuqtop  24167  utop2nei  24171  blval2  24483  caucfil  25216  ioorinv  25510  mbfss  25580  iblss2  25740  dvivthlem1  25946  lhop1  25952  deg1leb  26033  reeff1o  26390  sincosq3sgn  26442  sincosq4sgn  26443  dcubic  26789  efrlim  26912  efrlimOLD  26913  fsumharmonic  26955  isppw  27057  issqf  27079  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  ppiub  27148  lgsdinn0  27289  noetainflem4  27685  eqscut  27752  mulsprop  28075  elzs2  28329  elznns  28332  tglngne  28534  tgelrnln  28614  axlowdimlem14  28940  nbgrssovtx  29346  clwwlknclwwlkdif  29966  eupth2lem2  30206  fusgr2wsp2nb  30321  h2hlm  30967  isch2  31210  ch0pss  31432  nmcfnlbi  32039  jplem1  32255  hatomistici  32349  mdsymlem5  32394  cdjreui  32419  dfimafnf  32625  funcnvmpt  32656  fpwrelmap  32723  nn0min  32810  sgn3da  32824  wrdt2ind  32941  swrdrn3  32943  isarchi  33158  zarcls  33894  ordtconnlem1  33944  esumfsup  34090  esumpcvgval  34098  measvuni  34234  aean  34264  eulerpartlemgh  34398  ballotlemsima  34536  bnj1468  34865  subfacp1lem2a  35231  subfacp1lem6  35236  goeleq12bg  35400  dmopab3rexdif  35456  eldm3  35812  onsuct0  36492  bj-equsexvwd  36832  currysetlem1  36998  bj-restsn  37133  ptrest  37665  ptrecube  37666  poimirlem2  37668  poimirlem23  37689  sdclem2  37788  fdc  37791  fdc1  37792  istotbnd3  37817  sstotbnd  37821  prdstotbnd  37840  rrncmslem  37878  brinxprnres  38335  brcnvrabga  38380  alrmomodm  38397  br1cossxrnres  38556  lub0N  39294  glb0N  39298  cdlemefrs29bpre0  40501  dvhb1dimN  41091  dvhopellsm  41222  dibord  41264  dochnel2  41497  mapdvalc  41734  mapdval4N  41737  diophin  42870  diophun  42871  diophrex  42873  3rexfrabdioph  42895  6rexfrabdioph  42897  7rexfrabdioph  42898  zindbi  43044  tfsconcatrn  43440  rababg  43672  relexpnul  43776  clsk1independent  44144  scottabf  44338  hashnzfzclim  44420  fveqsb  44550  modelac8prim  45090  infxrbnd2  45472  cncfiooicclem1  45996  stoweidlem35  46138  tz6.12-afv  47278  ndmaovg  47289  tz6.12-afv2  47345  ich2exprop  47576  prprspr2  47623  usgrgrtrirex  48055  line2x  48860  line2y  48861  itsclc0b  48878  reuxfr1dd  48912  clddisj  49009  aacllem  49907