Theorem bitr3id 284

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitr3g  312  biass  385  imbibi  392  sbcom2  2160  19.16  2217  19.19  2221  necon1bbid  2980  rspc2gv  3577  elabgtOLD  3613  reuxfr1d  3694  sbceq1a  3736  sbcg  3804  sbcralt  3814  sbccsb2  4378  csbie2df  4384  reuprg0  4647  disjxun  5084  dmopab2rex  5846  dfres3  5915  xp11  6100  ressn  6210  fnssresb  6592  dmfco  6903  dffo4  7018  f1ompt  7024  funressn  7070  elunirnALT  7164  fliftf  7225  resoprab2  7434  elrnmpores  7452  ralrnmpo  7453  iunpw  7662  ordunisuc2  7736  tfis  7747  tfinds  7752  dfom2  7760  fiun  7831  f1iun  7832  opiota  7945  1stconst  7986  2ndconst  7987  fnsuppeq0  8056  iinon  8219  dfsmo2  8226  oeeui  8482  omabs  8530  brecop  8648  ixpsnf1o  8775  boxcutc  8778  ac6sfi  9130  wemapwe  9532  dmttrcl  9556  sdom2en01  10137  ac6num  10314  zorn2lem7  10337  ttukeylem6  10349  alephval2  10407  fpwwe2  10478  fpwwe  10481  nqereu  10764  suplem2pr  10888  map2psrpr  10945  supsrlem  10946  fimaxre3  12000  infm3  12013  crne0  12045  nn1suc  12074  xmulneg1  13082  supxrbnd1  13134  supxrbnd2  13135  iccneg  13283  wrdmap  14327  wrdind  14511  rtrclreclem3  14847  cnpart  15027  sqrt00  15051  lo1resb  15349  o1resb  15351  absefib  15983  efieq1re  15984  sadadd2lem2  16233  saddisjlem  16247  prmind2  16464  isprm7  16487  mreacs  17441  issubc  17624  isfunc  17653  pospo  18137  mndind  18540  eqgval  18878  resscntz  19011  frgpuplem  19450  qusabl  19538  dmdprd  19673  dprdcntz2  19713  dprd2d2  19719  isnzr2  20614  chrdvds  20812  chrcong  20813  znleval  20842  isphld  20939  mpfind  21397  gsummoncoe1  21555  pf1ind  21601  smadiadetr  21904  mp2pm2mplem4  22038  isclo  22318  ist1-2  22578  isnrm2  22589  bwth  22641  nconnsubb  22654  subislly  22712  ptclsg  22846  qtopcld  22944  kqcldsat  22964  qustgplem  23352  tsmssubm  23374  ustuqtop  23478  utop2nei  23482  blval2  23798  caucfil  24527  ioorinv  24820  mbfss  24890  iblss2  25050  dvivthlem1  25252  lhop1  25258  deg1leb  25340  reeff1o  25686  sincosq3sgn  25737  sincosq4sgn  25738  dcubic  26076  efrlim  26199  fsumharmonic  26241  isppw  26343  issqf  26365  fsumdvdsmul  26424  ppiub  26432  lgsdinn0  26573  tglngne  27044  tgelrnln  27124  axlowdimlem14  27456  nbgrssovtx  27861  clwwlknclwwlkdif  28475  eupth2lem2  28715  fusgr2wsp2nb  28830  h2hlm  29474  isch2  29717  ch0pss  29939  nmcfnlbi  30546  jplem1  30762  hatomistici  30856  mdsymlem5  30901  cdjreui  30926  dfimafnf  31102  funcnvmpt  31135  fpwrelmap  31199  nn0min  31265  wrdt2ind  31356  swrdrn3  31358  isarchi  31567  zarcls  31960  ordtconnlem1  32010  esumfsup  32174  esumpcvgval  32182  measvuni  32318  aean  32348  eulerpartlemgh  32481  ballotlemsima  32618  sgn3da  32644  bnj1468  32961  subfacp1lem2a  33277  subfacp1lem6  33282  goeleq12bg  33446  dmopab3rexdif  33502  eldm3  33858  naddid1  33959  noetainflem4  34013  eqscut  34069  onsuct0  34700  bj-equsexvwd  35033  currysetlem1  35205  bj-restsn  35330  ptrest  35853  ptrecube  35854  poimirlem2  35856  poimirlem23  35877  sdclem2  35977  fdc  35980  fdc1  35981  istotbnd3  36006  sstotbnd  36010  prdstotbnd  36029  rrncmslem  36067  brinxprnres  36529  brcnvrabga  36580  alrmomodm  36597  br1cossxrnres  36687  lub0N  37428  glb0N  37432  cdlemefrs29bpre0  38636  dvhb1dimN  39226  dvhopellsm  39357  dibord  39399  dochnel2  39632  mapdvalc  39869  mapdval4N  39872  diophin  40815  diophun  40816  diophrex  40818  3rexfrabdioph  40840  6rexfrabdioph  40842  7rexfrabdioph  40843  zindbi  40990  rababg  41420  relexpnul  41525  clsk1independent  41895  scottabf  42097  hashnzfzclim  42179  fveqsb  42310  infxrbnd2  43162  cncfiooicclem1  43689  stoweidlem35  43831  tz6.12-afv  44935  ndmaovg  44946  tz6.12-afv2  45002  ich2exprop  45193  prprspr2  45240  line2x  46370  line2y  46371  itsclc0b  46388  clddisj  46467  aacllem  46775