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  2178  19.16  2232  19.19  2236  necon1bbid  2969  rspc2gv  3572  reuxfr1d  3693  sbceq1a  3736  sbcg  3797  sbcralt  3806  sbccsb2  4367  csbie2df  4373  reuprg0  4636  disjxun  5072  dmopab2rex  5861  dfres3  5938  xp11  6128  ressn  6238  fnssresb  6609  dmfco  6925  funcnvmpt  6938  dffo4  7044  f1ompt  7052  funressn  7102  elunirnALT  7196  fliftf  7259  resoprab2  7475  elrnmpores  7494  ralrnmpo  7495  iunpw  7714  ordunisuc2  7784  tfis  7795  tfinds  7800  dfom2  7808  resf1extb  7874  fiun  7885  f1iun  7886  opiota  8001  1stconst  8039  2ndconst  8040  fnsuppeq0  8131  iinon  8269  dfsmo2  8276  oeeui  8527  omabs  8576  naddrid  8608  brecop  8746  ixpsnf1o  8875  boxcutc  8878  ac6sfi  9183  wemapwe  9607  dmttrcl  9631  sdom2en01  10213  ac6num  10390  zorn2lem7  10413  ttukeylem6  10425  alephval2  10484  fpwwe2  10555  fpwwe  10558  nqereu  10841  suplem2pr  10965  map2psrpr  11022  supsrlem  11023  fimaxre3  12091  infm3  12104  crne0  12141  nn1suc  12185  xmulneg1  13210  supxrbnd1  13262  supxrbnd2  13263  iccneg  13414  wrdmap  14497  wrdind  14673  rtrclreclem3  15011  cnpart  15191  sqrt00  15214  lo1resb  15515  o1resb  15517  absefib  16154  efieq1re  16155  sadadd2lem2  16408  saddisjlem  16422  prmind2  16643  isprm7  16667  mreacs  17613  issubc  17791  isfunc  17820  pospo  18298  mndind  18785  eqgval  19141  resscntz  19297  frgpuplem  19736  qusabl  19829  dmdprd  19964  dprdcntz2  20004  dprd2d2  20010  isnzr2  20484  chrdvds  21495  chrcong  21496  znleval  21523  isphld  21623  mpfind  22082  gsummoncoe1  22261  pf1ind  22308  smadiadetr  22628  mp2pm2mplem4  22762  isclo  23040  ist1-2  23300  isnrm2  23311  bwth  23363  nconnsubb  23376  subislly  23434  ptclsg  23568  qtopcld  23666  kqcldsat  23686  qustgplem  24074  tsmssubm  24096  ustuqtop  24199  utop2nei  24203  blval2  24515  caucfil  25238  ioorinv  25531  mbfss  25601  iblss2  25761  dvivthlem1  25963  lhop1  25969  deg1leb  26048  reeff1o  26400  sincosq3sgn  26452  sincosq4sgn  26453  dcubic  26798  efrlim  26921  fsumharmonic  26963  isppw  27065  issqf  27087  fsumdvdsmul  27146  ppiub  27155  lgsdinn0  27296  noetainflem4  27692  eqcuts  27765  mulsprop  28110  elzs2  28379  elznns  28382  tglngne  28606  tgelrnln  28686  axlowdimlem14  29012  nbgrssovtx  29418  clwwlknclwwlkdif  30037  eupth2lem2  30277  fusgr2wsp2nb  30392  h2hlm  31039  isch2  31282  ch0pss  31504  nmcfnlbi  32111  jplem1  32327  hatomistici  32421  mdsymlem5  32466  cdjreui  32491  dfimafnf  32697  fpwrelmap  32794  nn0min  32882  sgn3da  32895  wrdt2ind  33001  swrdrn3  33003  gsummptp1  33106  gsummulsubdishift1  33117  isarchi  33231  esplyind  33707  zarcls  34006  ordtconnlem1  34056  esumfsup  34202  esumpcvgval  34210  measvuni  34346  aean  34376  eulerpartlemgh  34510  ballotlemsima  34648  bnj1468  34976  subfacp1lem2a  35350  subfacp1lem6  35355  goeleq12bg  35519  dmopab3rexdif  35575  eldm3  35931  onsuct0  36611  bj-equsexvwd  37058  currysetlem1  37242  bj-restsn  37382  ptrest  37928  ptrecube  37929  poimirlem2  37931  poimirlem23  37952  sdclem2  38051  fdc  38054  fdc1  38055  istotbnd3  38080  sstotbnd  38084  prdstotbnd  38103  rrncmslem  38141  brinxprnres  38606  brcnvrabga  38651  alrmomodm  38668  br1cossxrnres  38847  lub0N  39623  glb0N  39627  cdlemefrs29bpre0  40830  dvhb1dimN  41420  dvhopellsm  41551  dibord  41593  dochnel2  41826  mapdvalc  42063  mapdval4N  42066  diophin  43192  diophun  43193  diophrex  43195  3rexfrabdioph  43213  6rexfrabdioph  43215  7rexfrabdioph  43216  zindbi  43362  tfsconcatrn  43758  rababg  43989  relexpnul  44093  clsk1independent  44461  scottabf  44655  hashnzfzclim  44737  fveqsb  44867  modelac8prim  45407  infxrbnd2  45786  cncfiooicclem1  46309  stoweidlem35  46451  tz6.12-afv  47609  ndmaovg  47620  tz6.12-afv2  47676  ich2exprop  47919  prprspr2  47966  usgrgrtrirex  48414  line2x  49218  line2y  49219  itsclc0b  49236  reuxfr1dd  49270  clddisj  49367  aacllem  50264