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  2174  19.16  2226  19.19  2230  necon1bbid  2964  rspc2gv  3598  reuxfr1d  3721  sbceq1a  3764  sbcg  3826  sbcralt  3835  sbccsb2  4400  csbie2df  4406  reuprg0  4666  disjxun  5105  dmopab2rex  5881  dfres3  5955  xp11  6148  ressn  6258  fnssresb  6640  dmfco  6957  dffo4  7075  f1ompt  7083  funressn  7131  elunirnALT  7226  fliftf  7290  resoprab2  7508  elrnmpores  7527  ralrnmpo  7528  iunpw  7747  ordunisuc2  7820  tfis  7831  tfinds  7836  dfom2  7844  resf1extb  7910  fiun  7921  f1iun  7922  opiota  8038  1stconst  8079  2ndconst  8080  fnsuppeq0  8171  iinon  8309  dfsmo2  8316  oeeui  8566  omabs  8615  naddrid  8647  brecop  8783  ixpsnf1o  8911  boxcutc  8914  ac6sfi  9231  wemapwe  9650  dmttrcl  9674  sdom2en01  10255  ac6num  10432  zorn2lem7  10455  ttukeylem6  10467  alephval2  10525  fpwwe2  10596  fpwwe  10599  nqereu  10882  suplem2pr  11006  map2psrpr  11063  supsrlem  11064  fimaxre3  12129  infm3  12142  crne0  12179  nn1suc  12208  xmulneg1  13229  supxrbnd1  13281  supxrbnd2  13282  iccneg  13433  wrdmap  14511  wrdind  14687  rtrclreclem3  15026  cnpart  15206  sqrt00  15229  lo1resb  15530  o1resb  15532  absefib  16166  efieq1re  16167  sadadd2lem2  16420  saddisjlem  16434  prmind2  16655  isprm7  16678  mreacs  17619  issubc  17797  isfunc  17826  pospo  18304  mndind  18755  eqgval  19109  resscntz  19265  frgpuplem  19702  qusabl  19795  dmdprd  19930  dprdcntz2  19970  dprd2d2  19976  isnzr2  20427  chrdvds  21436  chrcong  21437  znleval  21464  isphld  21563  mpfind  22014  gsummoncoe1  22195  pf1ind  22242  smadiadetr  22562  mp2pm2mplem4  22696  isclo  22974  ist1-2  23234  isnrm2  23245  bwth  23297  nconnsubb  23310  subislly  23368  ptclsg  23502  qtopcld  23600  kqcldsat  23620  qustgplem  24008  tsmssubm  24030  ustuqtop  24134  utop2nei  24138  blval2  24450  caucfil  25183  ioorinv  25477  mbfss  25547  iblss2  25707  dvivthlem1  25913  lhop1  25919  deg1leb  26000  reeff1o  26357  sincosq3sgn  26409  sincosq4sgn  26410  dcubic  26756  efrlim  26879  efrlimOLD  26880  fsumharmonic  26922  isppw  27024  issqf  27046  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  ppiub  27115  lgsdinn0  27256  noetainflem4  27652  eqscut  27717  mulsprop  28033  elzs2  28287  elznns  28290  tglngne  28477  tgelrnln  28557  axlowdimlem14  28882  nbgrssovtx  29288  clwwlknclwwlkdif  29908  eupth2lem2  30148  fusgr2wsp2nb  30263  h2hlm  30909  isch2  31152  ch0pss  31374  nmcfnlbi  31981  jplem1  32197  hatomistici  32291  mdsymlem5  32336  cdjreui  32361  dfimafnf  32560  funcnvmpt  32591  fpwrelmap  32656  nn0min  32745  sgn3da  32759  wrdt2ind  32875  swrdrn3  32877  isarchi  33136  zarcls  33864  ordtconnlem1  33914  esumfsup  34060  esumpcvgval  34068  measvuni  34204  aean  34234  eulerpartlemgh  34369  ballotlemsima  34507  bnj1468  34836  subfacp1lem2a  35167  subfacp1lem6  35172  goeleq12bg  35336  dmopab3rexdif  35392  eldm3  35748  onsuct0  36429  bj-equsexvwd  36769  currysetlem1  36935  bj-restsn  37070  ptrest  37613  ptrecube  37614  poimirlem2  37616  poimirlem23  37637  sdclem2  37736  fdc  37739  fdc1  37740  istotbnd3  37765  sstotbnd  37769  prdstotbnd  37788  rrncmslem  37826  brinxprnres  38279  brcnvrabga  38324  alrmomodm  38341  br1cossxrnres  38439  lub0N  39182  glb0N  39186  cdlemefrs29bpre0  40390  dvhb1dimN  40980  dvhopellsm  41111  dibord  41153  dochnel2  41386  mapdvalc  41623  mapdval4N  41626  diophin  42760  diophun  42761  diophrex  42763  3rexfrabdioph  42785  6rexfrabdioph  42787  7rexfrabdioph  42788  zindbi  42935  tfsconcatrn  43331  rababg  43563  relexpnul  43667  clsk1independent  44035  scottabf  44229  hashnzfzclim  44311  fveqsb  44442  modelac8prim  44982  infxrbnd2  45365  cncfiooicclem1  45891  stoweidlem35  46033  tz6.12-afv  47174  ndmaovg  47185  tz6.12-afv2  47241  ich2exprop  47472  prprspr2  47519  usgrgrtrirex  47949  line2x  48743  line2y  48744  itsclc0b  48761  reuxfr1dd  48795  clddisj  48892  aacllem  49790