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  2171  19.16  2223  19.19  2227  necon1bbid  2978  rspc2gv  3632  elabgtOLDOLD  3674  reuxfr1d  3759  sbceq1a  3802  sbcg  3870  sbcralt  3881  sbccsb2  4443  csbie2df  4449  reuprg0  4707  disjxun  5146  dmopab2rex  5931  dfres3  6005  xp11  6197  ressn  6307  fnssresb  6691  dmfco  7005  dffo4  7123  f1ompt  7131  funressn  7179  elunirnALT  7272  fliftf  7335  resoprab2  7552  elrnmpores  7571  ralrnmpo  7572  iunpw  7790  ordunisuc2  7865  tfis  7876  tfinds  7881  dfom2  7889  fiun  7966  f1iun  7967  opiota  8083  1stconst  8124  2ndconst  8125  fnsuppeq0  8216  iinon  8379  dfsmo2  8386  oeeui  8639  omabs  8688  naddrid  8720  brecop  8849  ixpsnf1o  8977  boxcutc  8980  ac6sfi  9318  wemapwe  9735  dmttrcl  9759  sdom2en01  10340  ac6num  10517  zorn2lem7  10540  ttukeylem6  10552  alephval2  10610  fpwwe2  10681  fpwwe  10684  nqereu  10967  suplem2pr  11091  map2psrpr  11148  supsrlem  11149  fimaxre3  12212  infm3  12225  crne0  12257  nn1suc  12286  xmulneg1  13308  supxrbnd1  13360  supxrbnd2  13361  iccneg  13509  wrdmap  14581  wrdind  14757  rtrclreclem3  15096  cnpart  15276  sqrt00  15299  lo1resb  15597  o1resb  15599  absefib  16231  efieq1re  16232  sadadd2lem2  16484  saddisjlem  16498  prmind2  16719  isprm7  16742  mreacs  17703  issubc  17886  isfunc  17915  pospo  18403  mndind  18854  eqgval  19208  resscntz  19364  frgpuplem  19805  qusabl  19898  dmdprd  20033  dprdcntz2  20073  dprd2d2  20079  isnzr2  20535  chrdvds  21559  chrcong  21560  znleval  21591  isphld  21690  mpfind  22149  gsummoncoe1  22328  pf1ind  22375  smadiadetr  22697  mp2pm2mplem4  22831  isclo  23111  ist1-2  23371  isnrm2  23382  bwth  23434  nconnsubb  23447  subislly  23505  ptclsg  23639  qtopcld  23737  kqcldsat  23757  qustgplem  24145  tsmssubm  24167  ustuqtop  24271  utop2nei  24275  blval2  24591  caucfil  25331  ioorinv  25625  mbfss  25695  iblss2  25856  dvivthlem1  26062  lhop1  26068  deg1leb  26149  reeff1o  26506  sincosq3sgn  26557  sincosq4sgn  26558  dcubic  26904  efrlim  27027  efrlimOLD  27028  fsumharmonic  27070  isppw  27172  issqf  27194  fsumdvdsmul  27253  fsumdvdsmulOLD  27255  ppiub  27263  lgsdinn0  27404  noetainflem4  27800  eqscut  27865  mulsprop  28171  elzs2  28400  elznns  28403  tglngne  28573  tgelrnln  28653  axlowdimlem14  28985  nbgrssovtx  29393  clwwlknclwwlkdif  30008  eupth2lem2  30248  fusgr2wsp2nb  30363  h2hlm  31009  isch2  31252  ch0pss  31474  nmcfnlbi  32081  jplem1  32297  hatomistici  32391  mdsymlem5  32436  cdjreui  32461  dfimafnf  32653  funcnvmpt  32684  fpwrelmap  32751  nn0min  32827  wrdt2ind  32923  swrdrn3  32925  isarchi  33172  zarcls  33835  ordtconnlem1  33885  esumfsup  34051  esumpcvgval  34059  measvuni  34195  aean  34225  eulerpartlemgh  34360  ballotlemsima  34497  sgn3da  34523  bnj1468  34839  subfacp1lem2a  35165  subfacp1lem6  35170  goeleq12bg  35334  dmopab3rexdif  35390  eldm3  35741  onsuct0  36424  bj-equsexvwd  36764  currysetlem1  36930  bj-restsn  37065  ptrest  37606  ptrecube  37607  poimirlem2  37609  poimirlem23  37630  sdclem2  37729  fdc  37732  fdc1  37733  istotbnd3  37758  sstotbnd  37762  prdstotbnd  37781  rrncmslem  37819  brinxprnres  38273  brcnvrabga  38324  alrmomodm  38341  br1cossxrnres  38430  lub0N  39171  glb0N  39175  cdlemefrs29bpre0  40379  dvhb1dimN  40969  dvhopellsm  41100  dibord  41142  dochnel2  41375  mapdvalc  41612  mapdval4N  41615  diophin  42760  diophun  42761  diophrex  42763  3rexfrabdioph  42785  6rexfrabdioph  42787  7rexfrabdioph  42788  zindbi  42935  tfsconcatrn  43332  rababg  43564  relexpnul  43668  clsk1independent  44036  scottabf  44236  hashnzfzclim  44318  fveqsb  44449  infxrbnd2  45319  cncfiooicclem1  45849  stoweidlem35  45991  tz6.12-afv  47123  ndmaovg  47134  tz6.12-afv2  47190  ich2exprop  47396  prprspr2  47443  usgrgrtrirex  47853  line2x  48604  line2y  48605  itsclc0b  48622  reuxfr1dd  48655  clddisj  48700  aacllem  49032