Theorem bitr3id 287

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitr3g  315  biass  387  imbibiOLD  395  sbcom2  2207  19.16  2261  19.19  2265  necon1bbid  2997  rspc2gv  3592  reuxfr1d  3714  sbceq1a  3756  sbcg  3817  sbcralt  3826  sbccsb2  4392  csbie2df  4398  reuprg0  4662  disjxun  5099  dmopab2rex  5894  dfres3  5970  xp11  6161  ressn  6272  fnssresb  6643  dmfco  6963  funcnvmpt  6977  dffo4  7084  f1ompt  7092  funressn  7142  elunirnALT  7236  fliftf  7299  resoprab2  7515  elrnmpores  7534  ralrnmpo  7535  iunpw  7754  ordunisuc2  7824  tfis  7835  tfinds  7840  dfom2  7848  resf1extb  7915  fiun  7924  f1iun  7925  opiota  8040  1stconst  8079  2ndconst  8080  fnsuppeq0  8172  iinon  8311  dfsmo2  8318  oeeui  8572  omabs  8621  naddrid  8654  brecop  8792  ixpsnf1o  8920  boxcutc  8923  ac6sfi  9228  wemapwe  9650  dmttrcl  9674  scottabf  9850  sdom2en01  10270  ac6num  10447  zorn2lem7  10470  ttukeylem6  10482  alephval2  10541  fpwwe2  10612  fpwwe  10615  nqereu  10898  suplem2pr  11022  map2psrpr  11079  supsrlem  11080  fimaxre3  12148  infm3  12161  crne0  12198  nn1suc  12242  xmulneg1  13282  supxrbnd1  13334  supxrbnd2  13335  iccneg  13486  wrdmap  14569  wrdind  14745  rtrclreclem3  15083  sgn3da  15124  cnpart  15277  sqrt00  15300  lo1resb  15601  o1resb  15603  absefib  16240  efieq1re  16241  sadadd2lem2  16494  saddisjlem  16508  prmind2  16729  isprm7  16753  mreacs  17700  issubc  17878  isfunc  17907  pospo  18385  mndind  18872  eqgval  19228  resscntz  19383  frgpuplem  19822  qusabl  19915  dmdprd  20050  dprdcntz2  20090  dprd2d2  20096  isnzr2  20578  chrdvds  21585  chrcong  21586  znleval  21613  isphld  21713  mpfind  22175  gsummoncoe1  22378  pf1ind  22425  smadiadetr  22742  mp2pm2mplem4  22876  isclo  23154  ist1-2  23414  isnrm2  23425  bwth  23477  nconnsubb  23490  subislly  23548  ptclsg  23682  qtopcld  23780  kqcldsat  23800  qustgplem  24188  tsmssubm  24210  ustuqtop  24313  utop2nei  24317  blval2  24629  caucfil  25352  ioorinv  25645  mbfss  25715  iblss2  25875  dvivthlem1  26077  lhop1  26083  deg1leb  26162  reeff1o  26517  sincosq3sgn  26572  sincosq4sgn  26573  dcubic  26918  efrlim  27041  fsumharmonic  27083  isppw  27185  issqf  27207  fsumdvdsmul  27266  ppiub  27275  lgsdinn0  27416  noetainflem4  27811  eqcuts  27885  mulsprop  28230  elzs2  28499  elznns  28502  tglngne  28726  tgelrnln  28806  tgelrnpln  28990  axlowdimlem14  29163  nbgrssovtx  29569  clwwlknclwwlkdif  30188  eupth2lem2  30428  fusgr2wsp2nb  30543  h2hlm  31190  isch2  31433  ch0pss  31655  nmcfnlbi  32262  jplem1  32478  hatomistici  32572  mdsymlem5  32617  cdjreui  32642  dfimafnf  32844  fpwrelmap  32941  nn0min  33029  wrdt2ind  33137  swrdrn3  33139  gsummptp1  33243  gsummulsubdishift1  33254  isarchi  33368  esplyind  33874  zarcls  34173  ordtconnlem1  34223  esumfsup  34369  esumpcvgval  34377  measvuni  34513  aean  34543  eulerpartlemgh  34677  ballotlemsima  34815  bnj1468  35143  subfacp1lem2a  35535  subfacp1lem6  35540  goeleq12bg  35704  dmopab3rexdif  35760  eldm3  36116  onsuct0  36806  bj-equsexvwd  37253  currysetlem1  37437  bj-restsn  37577  ptrest  38123  ptrecube  38124  poimirlem2  38126  poimirlem23  38147  sdclem2  38246  fdc  38249  fdc1  38250  istotbnd3  38275  sstotbnd  38279  prdstotbnd  38298  rrncmslem  38336  brinxprnres  38801  brcnvrabga  38846  alrmomodm  38863  br1cossxrnres  39042  lub0N  39818  glb0N  39822  cdlemefrs29bpre0  41025  dvhb1dimN  41615  dvhopellsm  41746  dibord  41788  dochnel2  42021  mapdvalc  42258  mapdval4N  42261  diophin  43358  diophun  43359  diophrex  43361  3rexfrabdioph  43379  6rexfrabdioph  43381  7rexfrabdioph  43382  zindbi  43528  tfsconcatrn  43924  rababg  44155  relexpnul  44259  clsk1independent  44627  hashnzfzclim  44889  fveqsb  45019  modelac8prim  45559  infxrbnd2  45935  cncfiooicclem1  46458  stoweidlem35  46600  tz6.12-afv  47758  ndmaovg  47769  tz6.12-afv2  47825  ich2exprop  48068  prprspr2  48115  usgrgrtrirex  48563  line2x  49367  line2y  49368  itsclc0b  49385  reuxfr1dd  49419  clddisj  49516  aacllem  50413