Theorem bitr3id 288

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr3g  316  biass  388  imbibiOLD  396  sbcom2  2206  19.16  2260  19.19  2264  necon1bbid  2996  rspc2gv  3590  reuxfr1d  3712  sbceq1a  3754  sbcg  3815  sbcralt  3824  sbccsb2  4401  csbie2df  4407  reuprg0  4667  disjxun  5106  dmopab2rex  5906  dfres3  5982  xp11  6172  ressn  6286  fnssresb  6657  dmfco  6977  funcnvmpt  6991  dffo4  7098  f1ompt  7106  funressn  7156  elunirnALT  7250  fliftf  7313  resoprab2  7531  elrnmpores  7550  ralrnmpo  7551  iunpw  7768  ordunisuc2  7838  tfis  7849  tfinds  7854  dfom2  7862  resf1extb  7929  fiun  7938  f1iun  7939  opiota  8054  1stconst  8093  2ndconst  8094  fnsuppeq0  8186  iinon  8325  dfsmo2  8332  oeeui  8586  omabs  8635  naddrid  8668  brecop  8806  ixpsnf1o  8934  boxcutc  8937  ac6sfi  9242  wemapwe  9664  dmttrcl  9688  scottabf  9866  sdom2en01  10292  ac6num  10469  zorn2lem7  10492  ttukeylem6  10504  alephval2  10563  fpwwe2  10634  fpwwe  10637  nqereu  10920  suplem2pr  11044  map2psrpr  11101  supsrlem  11102  fimaxre3  12167  infm3  12180  crne0  12217  nn1suc  12261  xmulneg1  13301  supxrbnd1  13353  supxrbnd2  13354  iccneg  13505  wrdmap  14590  wrdind  14766  rtrclreclem3  15104  sgn3da  15145  cnpart  15298  sqrt00  15321  lo1resb  15622  o1resb  15624  absefib  16260  efieq1re  16261  sadadd2lem2  16514  saddisjlem  16528  prmind2  16749  isprm7  16773  mreacs  17720  issubc  17898  isfunc  17927  pospo  18405  mndind  18893  eqgval  19251  resscntz  19409  frgpuplem  19848  qusabl  19941  dmdprd  20076  dprdcntz2  20116  dprd2d2  20122  isnzr2  20626  chrdvds  21687  chrcong  21688  znleval  21715  isphld  21815  mpfind  22277  gsummoncoe1  22479  pf1ind  22526  smadiadetr  22843  mp2pm2mplem4  22977  isclo  23255  ist1-2  23515  isnrm2  23526  bwth  23578  nconnsubb  23591  subislly  23649  ptclsg  23783  qtopcld  23881  kqcldsat  23901  qustgplem  24289  tsmssubm  24311  ustuqtop  24414  utop2nei  24418  blval2  24730  caucfil  25453  ioorinv  25746  mbfss  25816  iblss2  25976  dvivthlem1  26178  lhop1  26184  deg1leb  26263  reeff1o  26621  sincosq3sgn  26676  sincosq4sgn  26677  dcubic  27022  efrlim  27145  fsumharmonic  27187  isppw  27289  issqf  27311  fsumdvdsmul  27370  ppiub  27379  lgsdinn0  27520  noetainflem4  27915  eqcuts  27989  mulsprop  28334  elzs2  28603  elznns  28606  tglngne  28830  tgelrnln  28914  tgelrnpln  29069  axlowdimlem14  29316  nbgrssovtx  29722  clwwlknclwwlkdif  30341  eupth2lem2  30581  fusgr2wsp2nb  30696  h2hlm  31343  isch2  31586  ch0pss  31808  nmcfnlbi  32415  jplem1  32631  hatomistici  32725  mdsymlem5  32770  cdjreui  32795  dfimafnf  32992  fpwrelmap  33089  nn0min  33176  wrdt2ind  33282  swrdrn3  33284  gsummptp1  33386  gsummulsubdishift1  33397  isarchi  33511  esplyind  33974  zarcls  34273  ordtconnlem1  34323  esumfsup  34469  esumpcvgval  34477  measvuni  34613  aean  34643  eulerpartlemgh  34777  ballotlemsima  34915  bnj1468  35243  subfacp1lem2a  35680  subfacp1lem6  35685  goeleq12bg  35849  dmopab3rexdif  35905  eldm3  36261  onsuct0  36980  bj-equsexvwd  37426  currysetlem1  37611  bj-restsn  37752  ptrest  38298  ptrecube  38299  poimirlem2  38301  poimirlem23  38322  sdclem2  38421  fdc  38424  fdc1  38425  istotbnd3  38450  sstotbnd  38454  prdstotbnd  38473  rrncmslem  38511  brinxprnres  38974  brcnvrabga  39019  alrmomodm  39036  br1cossxrnres  39215  lub0N  39991  glb0N  39995  cdlemefrs29bpre0  41198  dvhb1dimN  41788  dvhopellsm  41919  dibord  41961  dochnel2  42194  mapdvalc  42431  mapdval4N  42434  diophin  43531  diophun  43532  diophrex  43534  3rexfrabdioph  43552  6rexfrabdioph  43554  7rexfrabdioph  43555  zindbi  43701  tfsconcatrn  44097  rababg  44328  relexpnul  44432  clsk1independent  44800  hashnzfzclim  45060  fveqsb  45189  modelac8prim  45729  infxrbnd2  46112  cncfiooicclem1  46635  stoweidlem35  46777  tz6.12-afv  47938  ndmaovg  47949  tz6.12-afv2  48005  ich2exprop  48248  prprspr2  48295  usgrgrtrirex  48743  line2x  49562  line2y  49563  itsclc0b  49580  reuxfr1dd  49613  clddisj  49710  aacllem  50649