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  383  imbibi  390  sbcom2  2162  19.16  2213  19.19  2217  necon1bbid  2969  rspc2gv  3616  elabgtOLDOLD  3659  reuxfr1d  3742  sbceq1a  3784  sbcg  3852  sbcralt  3862  sbccsb2  4436  csbie2df  4442  reuprg0  4708  disjxun  5147  dmopab2rex  5920  dfres3  5990  xp11  6181  ressn  6291  fnssresb  6678  dmfco  6993  dffo4  7112  f1ompt  7120  funressn  7168  elunirnALT  7262  fliftf  7322  resoprab2  7539  elrnmpores  7559  ralrnmpo  7560  iunpw  7774  ordunisuc2  7849  tfis  7860  tfinds  7865  dfom2  7873  fiun  7947  f1iun  7948  opiota  8064  1stconst  8105  2ndconst  8106  fnsuppeq0  8197  iinon  8361  dfsmo2  8368  oeeui  8623  omabs  8672  naddrid  8704  brecop  8829  ixpsnf1o  8957  boxcutc  8960  ac6sfi  9312  wemapwe  9722  dmttrcl  9746  sdom2en01  10327  ac6num  10504  zorn2lem7  10527  ttukeylem6  10539  alephval2  10597  fpwwe2  10668  fpwwe  10671  nqereu  10954  suplem2pr  11078  map2psrpr  11135  supsrlem  11136  fimaxre3  12193  infm3  12206  crne0  12238  nn1suc  12267  xmulneg1  13283  supxrbnd1  13335  supxrbnd2  13336  iccneg  13484  wrdmap  14532  wrdind  14708  rtrclreclem3  15043  cnpart  15223  sqrt00  15246  lo1resb  15544  o1resb  15546  absefib  16178  efieq1re  16179  sadadd2lem2  16428  saddisjlem  16442  prmind2  16659  isprm7  16682  mreacs  17641  issubc  17824  isfunc  17853  pospo  18340  mndind  18788  eqgval  19140  resscntz  19296  frgpuplem  19739  qusabl  19832  dmdprd  19967  dprdcntz2  20007  dprd2d2  20013  isnzr2  20469  chrdvds  21473  chrcong  21474  znleval  21505  isphld  21603  mpfind  22075  gsummoncoe1  22252  pf1ind  22299  smadiadetr  22621  mp2pm2mplem4  22755  isclo  23035  ist1-2  23295  isnrm2  23306  bwth  23358  nconnsubb  23371  subislly  23429  ptclsg  23563  qtopcld  23661  kqcldsat  23681  qustgplem  24069  tsmssubm  24091  ustuqtop  24195  utop2nei  24199  blval2  24515  caucfil  25255  ioorinv  25549  mbfss  25619  iblss2  25779  dvivthlem1  25985  lhop1  25991  deg1leb  26075  reeff1o  26429  sincosq3sgn  26480  sincosq4sgn  26481  dcubic  26823  efrlim  26946  efrlimOLD  26947  fsumharmonic  26989  isppw  27091  issqf  27113  fsumdvdsmul  27172  fsumdvdsmulOLD  27174  ppiub  27182  lgsdinn0  27323  noetainflem4  27719  eqscut  27784  mulsprop  28080  tglngne  28426  tgelrnln  28506  axlowdimlem14  28838  nbgrssovtx  29246  clwwlknclwwlkdif  29861  eupth2lem2  30101  fusgr2wsp2nb  30216  h2hlm  30862  isch2  31105  ch0pss  31327  nmcfnlbi  31934  jplem1  32150  hatomistici  32244  mdsymlem5  32289  cdjreui  32314  dfimafnf  32502  funcnvmpt  32534  fpwrelmap  32597  nn0min  32668  wrdt2ind  32763  swrdrn3  32765  isarchi  32982  zarcls  33606  ordtconnlem1  33656  esumfsup  33820  esumpcvgval  33828  measvuni  33964  aean  33994  eulerpartlemgh  34129  ballotlemsima  34266  sgn3da  34292  bnj1468  34608  subfacp1lem2a  34921  subfacp1lem6  34926  goeleq12bg  35090  dmopab3rexdif  35146  eldm3  35486  onsuct0  36056  bj-equsexvwd  36389  currysetlem1  36557  bj-restsn  36692  ptrest  37223  ptrecube  37224  poimirlem2  37226  poimirlem23  37247  sdclem2  37346  fdc  37349  fdc1  37350  istotbnd3  37375  sstotbnd  37379  prdstotbnd  37398  rrncmslem  37436  brinxprnres  37893  brcnvrabga  37944  alrmomodm  37961  br1cossxrnres  38050  lub0N  38791  glb0N  38795  cdlemefrs29bpre0  39999  dvhb1dimN  40589  dvhopellsm  40720  dibord  40762  dochnel2  40995  mapdvalc  41232  mapdval4N  41235  diophin  42334  diophun  42335  diophrex  42337  3rexfrabdioph  42359  6rexfrabdioph  42361  7rexfrabdioph  42362  zindbi  42509  tfsconcatrn  42913  rababg  43146  relexpnul  43250  clsk1independent  43618  scottabf  43819  hashnzfzclim  43901  fveqsb  44032  infxrbnd2  44889  cncfiooicclem1  45419  stoweidlem35  45561  tz6.12-afv  46691  ndmaovg  46702  tz6.12-afv2  46758  ich2exprop  46948  prprspr2  46995  line2x  48013  line2y  48014  itsclc0b  48031  clddisj  48108  aacllem  48420