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	syl5bb 286	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr3g  317  biass  390  sbcom2  2166  19.16  2226  19.19  2230  sbbibOLD  2286  sbal2OLD  2551  necon1bbid  2988  rspc2gv  3548  elabgt  3580  reuxfr1d  3661  sbceq1a  3704  sbcralt  3774  sbccsb2  4324  csbie2df  4330  reuprg0  4588  disjxun  5023  dmopab2rex  5750  dfres3  5821  xp11  5997  ressn  6107  fnssresb  6445  dmfco  6741  dffo4  6853  f1ompt  6859  funressn  6905  elunirnALT  6996  fliftf  7055  resoprab2  7258  elrnmpores  7276  ralrnmpo  7277  iunpw  7485  ordunisuc2  7551  tfis  7561  tfinds  7566  dfom2  7574  fiun  7641  f1iun  7642  opiota  7754  1stconst  7793  2ndconst  7794  fnsuppeq0  7859  iinon  7980  dfsmo2  7987  oeeui  8231  omabs  8277  brecop  8393  ixpsnf1o  8513  boxcutc  8516  ac6sfi  8780  wemapwe  9178  sdom2en01  9747  ac6num  9924  zorn2lem7  9947  ttukeylem6  9959  alephval2  10017  fpwwe2  10088  fpwwe  10091  nqereu  10374  suplem2pr  10498  map2psrpr  10555  supsrlem  10556  fimaxre3  11609  infm3  11621  crne0  11652  nn1suc  11681  xmulneg1  12688  supxrbnd1  12740  supxrbnd2  12741  iccneg  12889  wrdmap  13930  wrdind  14116  rtrclreclem3  14452  cnpart  14632  sqrt00  14656  lo1resb  14954  o1resb  14956  absefib  15584  efieq1re  15585  sadadd2lem2  15834  saddisjlem  15848  prmind2  16066  isprm7  16089  mreacs  16972  issubc  17149  isfunc  17178  pospo  17634  mndind  18043  eqgval  18381  resscntz  18514  frgpuplem  18950  qusabl  19038  dmdprd  19173  dprdcntz2  19213  dprd2d2  19219  isnzr2  20089  chrdvds  20281  chrcong  20282  znleval  20307  isphld  20404  mpfind  20855  gsummoncoe1  21013  pf1ind  21059  smadiadetr  21360  mp2pm2mplem4  21494  isclo  21772  ist1-2  22032  isnrm2  22043  bwth  22095  nconnsubb  22108  subislly  22166  ptclsg  22300  qtopcld  22398  kqcldsat  22418  qustgplem  22806  tsmssubm  22828  ustuqtop  22932  utop2nei  22936  blval2  23249  caucfil  23968  ioorinv  24261  mbfss  24331  iblss2  24490  dvivthlem1  24692  lhop1  24698  deg1leb  24780  reeff1o  25126  sincosq3sgn  25177  sincosq4sgn  25178  dcubic  25516  efrlim  25639  fsumharmonic  25681  isppw  25783  issqf  25805  fsumdvdsmul  25864  ppiub  25872  lgsdinn0  26013  tglngne  26428  tgelrnln  26508  axlowdimlem14  26833  nbgrssovtx  27235  clwwlknclwwlkdif  27848  eupth2lem2  28088  fusgr2wsp2nb  28203  h2hlm  28847  isch2  29090  ch0pss  29312  nmcfnlbi  29919  jplem1  30135  hatomistici  30229  mdsymlem5  30274  cdjreui  30299  dfimafnf  30478  funcnvmpt  30513  fpwrelmap  30577  nn0min  30643  wrdt2ind  30734  swrdrn3  30736  isarchi  30947  zarcls  31330  ordtconnlem1  31380  esumfsup  31542  esumpcvgval  31550  measvuni  31686  aean  31716  eulerpartlemgh  31849  ballotlemsima  31986  sgn3da  32012  bnj1468  32331  subfacp1lem2a  32643  subfacp1lem6  32648  goeleq12bg  32812  dmopab3rexdif  32868  eldm3  33229  noetainflem4  33493  eqscut  33545  onsuct0  34164  currysetlem1  34648  bj-restsn  34762  ptrest  35321  ptrecube  35322  poimirlem2  35324  poimirlem23  35345  sdclem2  35445  fdc  35448  fdc1  35449  istotbnd3  35474  sstotbnd  35478  prdstotbnd  35497  rrncmslem  35535  brinxprnres  35973  brcnvrabga  36024  alrmomodm  36038  br1cossxrnres  36113  lub0N  36750  glb0N  36754  cdlemefrs29bpre0  37957  dvhb1dimN  38547  dvhopellsm  38678  dibord  38720  dochnel2  38953  mapdvalc  39190  mapdval4N  39193  diophin  40071  diophun  40072  diophrex  40074  3rexfrabdioph  40096  6rexfrabdioph  40098  7rexfrabdioph  40099  zindbi  40245  rababg  40631  relexpnul  40737  clsk1independent  41107  scottabf  41306  hashnzfzclim  41384  fveqsb  41515  infxrbnd2  42354  cncfiooicclem1  42886  stoweidlem35  43028  tz6.12-afv  44082  ndmaovg  44093  tz6.12-afv2  44149  ich2exprop  44341  prprspr2  44388  line2x  45518  line2y  45519  itsclc0b  45536  aacllem  45679