Theorem bitr3id 284

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitr3g  312  biass  383  imbibi  390  sbcom2  2159  19.16  2216  19.19  2220  necon1bbid  2978  rspc2gv  3620  elabgtOLD  3662  reuxfr1d  3745  sbceq1a  3787  sbcg  3855  sbcralt  3865  sbccsb2  4433  csbie2df  4439  reuprg0  4705  disjxun  5145  dmopab2rex  5916  dfres3  5985  xp11  6173  ressn  6283  fnssresb  6671  dmfco  6986  dffo4  7103  f1ompt  7111  funressn  7158  elunirnALT  7253  fliftf  7314  resoprab2  7529  elrnmpores  7548  ralrnmpo  7549  iunpw  7760  ordunisuc2  7835  tfis  7846  tfinds  7851  dfom2  7859  fiun  7931  f1iun  7932  opiota  8047  1stconst  8088  2ndconst  8089  fnsuppeq0  8179  iinon  8342  dfsmo2  8349  oeeui  8604  omabs  8652  naddrid  8684  brecop  8806  ixpsnf1o  8934  boxcutc  8937  ac6sfi  9289  wemapwe  9694  dmttrcl  9718  sdom2en01  10299  ac6num  10476  zorn2lem7  10499  ttukeylem6  10511  alephval2  10569  fpwwe2  10640  fpwwe  10643  nqereu  10926  suplem2pr  11050  map2psrpr  11107  supsrlem  11108  fimaxre3  12164  infm3  12177  crne0  12209  nn1suc  12238  xmulneg1  13252  supxrbnd1  13304  supxrbnd2  13305  iccneg  13453  wrdmap  14500  wrdind  14676  rtrclreclem3  15011  cnpart  15191  sqrt00  15214  lo1resb  15512  o1resb  15514  absefib  16145  efieq1re  16146  sadadd2lem2  16395  saddisjlem  16409  prmind2  16626  isprm7  16649  mreacs  17606  issubc  17789  isfunc  17818  pospo  18302  mndind  18745  eqgval  19093  resscntz  19238  frgpuplem  19681  qusabl  19774  dmdprd  19909  dprdcntz2  19949  dprd2d2  19955  isnzr2  20409  df2idl2  21009  chrdvds  21299  chrcong  21300  znleval  21329  isphld  21426  mpfind  21889  gsummoncoe1  22048  pf1ind  22094  smadiadetr  22397  mp2pm2mplem4  22531  isclo  22811  ist1-2  23071  isnrm2  23082  bwth  23134  nconnsubb  23147  subislly  23205  ptclsg  23339  qtopcld  23437  kqcldsat  23457  qustgplem  23845  tsmssubm  23867  ustuqtop  23971  utop2nei  23975  blval2  24291  caucfil  25031  ioorinv  25325  mbfss  25395  iblss2  25555  dvivthlem1  25760  lhop1  25766  deg1leb  25848  reeff1o  26195  sincosq3sgn  26246  sincosq4sgn  26247  dcubic  26587  efrlim  26710  fsumharmonic  26752  isppw  26854  issqf  26876  fsumdvdsmul  26935  ppiub  26943  lgsdinn0  27084  noetainflem4  27479  eqscut  27543  mulsprop  27825  tglngne  28068  tgelrnln  28148  axlowdimlem14  28480  nbgrssovtx  28885  clwwlknclwwlkdif  29499  eupth2lem2  29739  fusgr2wsp2nb  29854  h2hlm  30500  isch2  30743  ch0pss  30965  nmcfnlbi  31572  jplem1  31788  hatomistici  31882  mdsymlem5  31927  cdjreui  31952  dfimafnf  32127  funcnvmpt  32159  fpwrelmap  32225  nn0min  32293  wrdt2ind  32384  swrdrn3  32386  isarchi  32598  zarcls  33152  ordtconnlem1  33202  esumfsup  33366  esumpcvgval  33374  measvuni  33510  aean  33540  eulerpartlemgh  33675  ballotlemsima  33812  sgn3da  33838  bnj1468  34155  subfacp1lem2a  34469  subfacp1lem6  34474  goeleq12bg  34638  dmopab3rexdif  34694  eldm3  35035  onsuct0  35629  bj-equsexvwd  35962  currysetlem1  36131  bj-restsn  36266  ptrest  36790  ptrecube  36791  poimirlem2  36793  poimirlem23  36814  sdclem2  36913  fdc  36916  fdc1  36917  istotbnd3  36942  sstotbnd  36946  prdstotbnd  36965  rrncmslem  37003  brinxprnres  37463  brcnvrabga  37514  alrmomodm  37531  br1cossxrnres  37621  lub0N  38362  glb0N  38366  cdlemefrs29bpre0  39570  dvhb1dimN  40160  dvhopellsm  40291  dibord  40333  dochnel2  40566  mapdvalc  40803  mapdval4N  40806  diophin  41812  diophun  41813  diophrex  41815  3rexfrabdioph  41837  6rexfrabdioph  41839  7rexfrabdioph  41840  zindbi  41987  tfsconcatrn  42394  rababg  42627  relexpnul  42731  clsk1independent  43099  scottabf  43301  hashnzfzclim  43383  fveqsb  43514  infxrbnd2  44377  cncfiooicclem1  44907  stoweidlem35  45049  tz6.12-afv  46179  ndmaovg  46190  tz6.12-afv2  46246  ich2exprop  46437  prprspr2  46484  line2x  47527  line2y  47528  itsclc0b  47545  clddisj  47623  aacllem  47935