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  2175  19.16  2227  19.19  2231  necon1bbid  2965  rspc2gv  3585  reuxfr1d  3707  sbceq1a  3750  sbcg  3812  sbcralt  3821  sbccsb2  4385  csbie2df  4391  reuprg0  4653  disjxun  5087  dmopab2rex  5855  dfres3  5930  xp11  6119  ressn  6228  fnssresb  6599  dmfco  6913  dffo4  7031  f1ompt  7039  funressn  7087  elunirnALT  7181  fliftf  7244  resoprab2  7460  elrnmpores  7479  ralrnmpo  7480  iunpw  7699  ordunisuc2  7769  tfis  7780  tfinds  7785  dfom2  7793  resf1extb  7859  fiun  7870  f1iun  7871  opiota  7986  1stconst  8025  2ndconst  8026  fnsuppeq0  8117  iinon  8255  dfsmo2  8262  oeeui  8512  omabs  8561  naddrid  8593  brecop  8729  ixpsnf1o  8857  boxcutc  8860  ac6sfi  9163  wemapwe  9582  dmttrcl  9606  sdom2en01  10185  ac6num  10362  zorn2lem7  10385  ttukeylem6  10397  alephval2  10455  fpwwe2  10526  fpwwe  10529  nqereu  10812  suplem2pr  10936  map2psrpr  10993  supsrlem  10994  fimaxre3  12060  infm3  12073  crne0  12110  nn1suc  12139  xmulneg1  13160  supxrbnd1  13212  supxrbnd2  13213  iccneg  13364  wrdmap  14445  wrdind  14621  rtrclreclem3  14959  cnpart  15139  sqrt00  15162  lo1resb  15463  o1resb  15465  absefib  16099  efieq1re  16100  sadadd2lem2  16353  saddisjlem  16367  prmind2  16588  isprm7  16611  mreacs  17556  issubc  17734  isfunc  17763  pospo  18241  mndind  18728  eqgval  19082  resscntz  19238  frgpuplem  19677  qusabl  19770  dmdprd  19905  dprdcntz2  19945  dprd2d2  19951  isnzr2  20426  chrdvds  21456  chrcong  21457  znleval  21484  isphld  21584  mpfind  22035  gsummoncoe1  22216  pf1ind  22263  smadiadetr  22583  mp2pm2mplem4  22717  isclo  22995  ist1-2  23255  isnrm2  23266  bwth  23318  nconnsubb  23331  subislly  23389  ptclsg  23523  qtopcld  23621  kqcldsat  23641  qustgplem  24029  tsmssubm  24051  ustuqtop  24154  utop2nei  24158  blval2  24470  caucfil  25203  ioorinv  25497  mbfss  25567  iblss2  25727  dvivthlem1  25933  lhop1  25939  deg1leb  26020  reeff1o  26377  sincosq3sgn  26429  sincosq4sgn  26430  dcubic  26776  efrlim  26899  efrlimOLD  26900  fsumharmonic  26942  isppw  27044  issqf  27066  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  ppiub  27135  lgsdinn0  27276  noetainflem4  27672  eqscut  27739  mulsprop  28062  elzs2  28316  elznns  28319  tglngne  28521  tgelrnln  28601  axlowdimlem14  28926  nbgrssovtx  29332  clwwlknclwwlkdif  29949  eupth2lem2  30189  fusgr2wsp2nb  30304  h2hlm  30950  isch2  31193  ch0pss  31415  nmcfnlbi  32022  jplem1  32238  hatomistici  32332  mdsymlem5  32377  cdjreui  32402  dfimafnf  32608  funcnvmpt  32639  fpwrelmap  32706  nn0min  32793  sgn3da  32807  wrdt2ind  32924  swrdrn3  32926  isarchi  33141  zarcls  33877  ordtconnlem1  33927  esumfsup  34073  esumpcvgval  34081  measvuni  34217  aean  34247  eulerpartlemgh  34381  ballotlemsima  34519  bnj1468  34848  subfacp1lem2a  35192  subfacp1lem6  35197  goeleq12bg  35361  dmopab3rexdif  35417  eldm3  35773  onsuct0  36454  bj-equsexvwd  36794  currysetlem1  36960  bj-restsn  37095  ptrest  37638  ptrecube  37639  poimirlem2  37641  poimirlem23  37662  sdclem2  37761  fdc  37764  fdc1  37765  istotbnd3  37790  sstotbnd  37794  prdstotbnd  37813  rrncmslem  37851  brinxprnres  38304  brcnvrabga  38349  alrmomodm  38366  br1cossxrnres  38464  lub0N  39207  glb0N  39211  cdlemefrs29bpre0  40414  dvhb1dimN  41004  dvhopellsm  41135  dibord  41177  dochnel2  41410  mapdvalc  41647  mapdval4N  41650  diophin  42784  diophun  42785  diophrex  42787  3rexfrabdioph  42809  6rexfrabdioph  42811  7rexfrabdioph  42812  zindbi  42958  tfsconcatrn  43354  rababg  43586  relexpnul  43690  clsk1independent  44058  scottabf  44252  hashnzfzclim  44334  fveqsb  44464  modelac8prim  45004  infxrbnd2  45386  cncfiooicclem1  45910  stoweidlem35  46052  tz6.12-afv  47183  ndmaovg  47194  tz6.12-afv2  47250  ich2exprop  47481  prprspr2  47528  usgrgrtrirex  47960  line2x  48765  line2y  48766  itsclc0b  48783  reuxfr1dd  48817  clddisj  48914  aacllem  49812