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  397  sbcom2  2209  19.16  2263  19.19  2267  necon1bbid  2996  rspc2gv  3589  reuxfr1d  3711  sbceq1a  3753  sbcg  3814  sbcralt  3822  sbccsb2  4398  csbie2df  4404  reuprg0  4666  disjxun  5105  dmopab2rex  5905  dfres3  5981  xp11  6172  ressn  6287  fnssresb  6658  dmfco  6978  funcnvmpt  6992  dffo4  7099  f1ompt  7107  funressn  7159  elunirnALT  7252  fliftf  7319  resoprab2  7535  elrnmpores  7554  ralrnmpo  7555  iunpw  7773  ordunisuc2  7843  tfis  7854  tfinds  7859  dfom2  7867  resf1extb  7934  fiun  7943  f1iun  7944  opiota  8059  1stconst  8100  2ndconst  8101  fnsuppeq0  8193  iinon  8332  dfsmo2  8339  oeeui  8593  omabs  8642  naddrid  8675  brecop  8813  ixpsnf1o  8948  boxcutc  8951  ac6sfi  9257  wemapwe  9679  dmttrcl  9703  scottabf  9881  sdom2en01  10307  ac6num  10484  zorn2lem7  10507  ttukeylem6  10519  alephval2  10584  fpwwe2  10655  fpwwe  10658  nqereu  10941  suplem2pr  11065  map2psrpr  11122  supsrlem  11123  fimaxre3  12188  infm3  12201  crne0  12238  nn1suc  12282  xmulneg1  13323  supxrbnd1  13375  supxrbnd2  13376  iccneg  13527  wrdmap  14613  swrdrn3  14724  wrdind  14793  rtrclreclem3  15135  sgn3da  15176  cnpart  15329  sqrt00  15352  lo1resb  15653  o1resb  15655  absefib  16290  efieq1re  16291  sadadd2lem2  16544  saddisjlem  16558  prmind2  16779  isprm7  16803  mreacs  17750  issubc  17928  isfunc  17957  pospo  18435  mndind  18938  eqgval  19303  resscntz  19461  frgpuplem  19900  qusabl  19993  dmdprd  20128  dprdcntz2  20168  dprd2d2  20174  isnzr2  20679  chrdvds  21740  chrcong  21741  znleval  21768  isphld  21868  mpfind  22332  gsummoncoe1  22534  pf1ind  22581  smadiadetr  22898  mp2pm2mplem4  23035  isclo  23313  ist1-2  23573  isnrm2  23584  bwth  23636  nconnsubb  23649  subislly  23708  ptclsg  23842  qtopcld  23940  kqcldsat  23960  qustgplem  24348  tsmssubm  24370  ustuqtop  24473  utop2nei  24477  blval2  24789  caucfil  25512  ioorinv  25805  mbfss  25875  iblss2  26035  dvivthlem1  26237  lhop1  26243  deg1leb  26322  reeff1o  26680  sincosq3sgn  26735  sincosq4sgn  26736  dcubic  27081  efrlim  27204  fsumharmonic  27246  isppw  27348  issqf  27370  fsumdvdsmul  27429  ppiub  27438  lgsdinn0  27579  noetainflem4  27974  eqcuts  28048  mulsprop  28393  elzs2  28662  elznns  28665  tglngne  28890  tgelrnln  28975  tgelrnpln  29131  axlowdimlem14  29398  nbgrssovtx  29807  clwwlknclwwlkdif  30435  eupth2lem2  30685  fusgr2wsp2nb  30800  h2hlm  31447  isch2  31690  ch0pss  31912  nmcfnlbi  32519  jplem1  32735  hatomistici  32829  mdsymlem5  32874  cdjreui  32899  dfimafnf  33096  fpwrelmap  33191  nn0min  33278  wrdt2ind  33382  gsummptp1  33484  gsummulsubdishift1  33495  isarchi  33609  esplyind  34072  zarcls  34371  ordtconnlem1  34421  esumfsup  34567  esumpcvgval  34575  measvuni  34712  aean  34742  eulerpartlemgh  34876  ballotlemsima  35014  bnj1468  35342  subfacp1lem2a  35746  subfacp1lem6  35751  goeleq12bg  35915  dmopab3rexdif  35971  eldm3  36327  onsuct0  37047  bj-equsexvwd  37493  currysetlem1  37678  bj-restsn  37819  ptrest  38355  ptrecube  38356  poimirlem2  38358  poimirlem23  38379  sdclem2  38479  fdc  38482  fdc1  38483  istotbnd3  38508  sstotbnd  38512  prdstotbnd  38531  rrncmslem  38569  brinxprnres  39032  brcnvrabga  39077  alrmomodm  39094  br1cossxrnres  39273  lub0N  40049  glb0N  40053  cdlemefrs29bpre0  41256  dvhb1dimN  41846  dvhopellsm  41977  dibord  42019  dochnel2  42252  mapdvalc  42489  mapdval4N  42492  diophin  43604  diophun  43605  diophrex  43607  3rexfrabdioph  43625  6rexfrabdioph  43627  7rexfrabdioph  43628  zindbi  43774  tfsconcatrn  44170  rababg  44401  relexpnul  44505  clsk1independent  44873  hashnzfzclim  45133  fveqsb  45262  modelac8prim  45802  infxrbnd2  46185  cncfiooicclem1  46708  stoweidlem35  46850  tz6.12-afv  48048  ndmaovg  48059  tz6.12-afv2  48115  ich2exprop  48358  prprspr2  48405  usgrgrtrirex  48853  line2x  49671  line2y  49672  itsclc0b  49689  reuxfr1dd  49722  clddisj  49817  aacllem  50759