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  2179  19.16  2233  19.19  2237  necon1bbid  2972  rspc2gv  3587  reuxfr1d  3709  sbceq1a  3752  sbcg  3814  sbcralt  3823  sbccsb2  4390  csbie2df  4396  reuprg0  4660  disjxun  5097  dmopab2rex  5867  dfres3  5944  xp11  6134  ressn  6244  fnssresb  6615  dmfco  6931  funcnvmpt  6944  dffo4  7050  f1ompt  7058  funressn  7106  elunirnALT  7200  fliftf  7263  resoprab2  7479  elrnmpores  7498  ralrnmpo  7499  iunpw  7718  ordunisuc2  7788  tfis  7799  tfinds  7804  dfom2  7812  resf1extb  7878  fiun  7889  f1iun  7890  opiota  8005  1stconst  8044  2ndconst  8045  fnsuppeq0  8136  iinon  8274  dfsmo2  8281  oeeui  8532  omabs  8581  naddrid  8613  brecop  8751  ixpsnf1o  8880  boxcutc  8883  ac6sfi  9188  wemapwe  9610  dmttrcl  9634  sdom2en01  10216  ac6num  10393  zorn2lem7  10416  ttukeylem6  10428  alephval2  10487  fpwwe2  10558  fpwwe  10561  nqereu  10844  suplem2pr  10968  map2psrpr  11025  supsrlem  11026  fimaxre3  12092  infm3  12105  crne0  12142  nn1suc  12171  xmulneg1  13188  supxrbnd1  13240  supxrbnd2  13241  iccneg  13392  wrdmap  14473  wrdind  14649  rtrclreclem3  14987  cnpart  15167  sqrt00  15190  lo1resb  15491  o1resb  15493  absefib  16127  efieq1re  16128  sadadd2lem2  16381  saddisjlem  16395  prmind2  16616  isprm7  16639  mreacs  17585  issubc  17763  isfunc  17792  pospo  18270  mndind  18757  eqgval  19110  resscntz  19266  frgpuplem  19705  qusabl  19798  dmdprd  19933  dprdcntz2  19973  dprd2d2  19979  isnzr2  20455  chrdvds  21485  chrcong  21486  znleval  21513  isphld  21613  mpfind  22074  gsummoncoe1  22256  pf1ind  22303  smadiadetr  22623  mp2pm2mplem4  22757  isclo  23035  ist1-2  23295  isnrm2  23306  bwth  23358  nconnsubb  23371  subislly  23429  ptclsg  23563  qtopcld  23661  kqcldsat  23681  qustgplem  24069  tsmssubm  24091  ustuqtop  24194  utop2nei  24198  blval2  24510  caucfil  25243  ioorinv  25537  mbfss  25607  iblss2  25767  dvivthlem1  25973  lhop1  25979  deg1leb  26060  reeff1o  26417  sincosq3sgn  26469  sincosq4sgn  26470  dcubic  26816  efrlim  26939  efrlimOLD  26940  fsumharmonic  26982  isppw  27084  issqf  27106  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  ppiub  27175  lgsdinn0  27316  noetainflem4  27712  eqscut  27783  mulsprop  28112  elzs2  28378  elznns  28381  tglngne  28605  tgelrnln  28685  axlowdimlem14  29011  nbgrssovtx  29417  clwwlknclwwlkdif  30037  eupth2lem2  30277  fusgr2wsp2nb  30392  h2hlm  31038  isch2  31281  ch0pss  31503  nmcfnlbi  32110  jplem1  32326  hatomistici  32420  mdsymlem5  32465  cdjreui  32490  dfimafnf  32696  fpwrelmap  32793  nn0min  32882  sgn3da  32896  wrdt2ind  33016  swrdrn3  33018  gsummptp1  33121  gsummulsubdishift1  33132  isarchi  33245  esplyind  33712  zarcls  34012  ordtconnlem1  34062  esumfsup  34208  esumpcvgval  34216  measvuni  34352  aean  34382  eulerpartlemgh  34516  ballotlemsima  34654  bnj1468  34983  subfacp1lem2a  35355  subfacp1lem6  35360  goeleq12bg  35524  dmopab3rexdif  35580  eldm3  35936  onsuct0  36616  bj-equsexvwd  36957  currysetlem1  37123  bj-restsn  37258  ptrest  37791  ptrecube  37792  poimirlem2  37794  poimirlem23  37815  sdclem2  37914  fdc  37917  fdc1  37918  istotbnd3  37943  sstotbnd  37947  prdstotbnd  37966  rrncmslem  38004  brinxprnres  38469  brcnvrabga  38514  alrmomodm  38531  br1cossxrnres  38710  lub0N  39486  glb0N  39490  cdlemefrs29bpre0  40693  dvhb1dimN  41283  dvhopellsm  41414  dibord  41456  dochnel2  41689  mapdvalc  41926  mapdval4N  41929  diophin  43050  diophun  43051  diophrex  43053  3rexfrabdioph  43075  6rexfrabdioph  43077  7rexfrabdioph  43078  zindbi  43224  tfsconcatrn  43620  rababg  43851  relexpnul  43955  clsk1independent  44323  scottabf  44517  hashnzfzclim  44599  fveqsb  44729  modelac8prim  45269  infxrbnd2  45649  cncfiooicclem1  46173  stoweidlem35  46315  tz6.12-afv  47455  ndmaovg  47466  tz6.12-afv2  47522  ich2exprop  47753  prprspr2  47800  usgrgrtrirex  48232  line2x  49036  line2y  49037  itsclc0b  49054  reuxfr1dd  49088  clddisj  49185  aacllem  50082