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  2174  19.16  2226  19.19  2230  necon1bbid  2986  rspc2gv  3645  elabgtOLDOLD  3687  reuxfr1d  3772  sbceq1a  3815  sbcg  3883  sbcralt  3894  sbccsb2  4460  csbie2df  4466  reuprg0  4727  disjxun  5164  dmopab2rex  5942  dfres3  6014  xp11  6206  ressn  6316  fnssresb  6702  dmfco  7018  dffo4  7137  f1ompt  7145  funressn  7193  elunirnALT  7289  fliftf  7351  resoprab2  7569  elrnmpores  7588  ralrnmpo  7589  iunpw  7806  ordunisuc2  7881  tfis  7892  tfinds  7897  dfom2  7905  fiun  7983  f1iun  7984  opiota  8100  1stconst  8141  2ndconst  8142  fnsuppeq0  8233  iinon  8396  dfsmo2  8403  oeeui  8658  omabs  8707  naddrid  8739  brecop  8868  ixpsnf1o  8996  boxcutc  8999  ac6sfi  9348  wemapwe  9766  dmttrcl  9790  sdom2en01  10371  ac6num  10548  zorn2lem7  10571  ttukeylem6  10583  alephval2  10641  fpwwe2  10712  fpwwe  10715  nqereu  10998  suplem2pr  11122  map2psrpr  11179  supsrlem  11180  fimaxre3  12241  infm3  12254  crne0  12286  nn1suc  12315  xmulneg1  13331  supxrbnd1  13383  supxrbnd2  13384  iccneg  13532  wrdmap  14594  wrdind  14770  rtrclreclem3  15109  cnpart  15289  sqrt00  15312  lo1resb  15610  o1resb  15612  absefib  16246  efieq1re  16247  sadadd2lem2  16496  saddisjlem  16510  prmind2  16732  isprm7  16755  mreacs  17716  issubc  17899  isfunc  17928  pospo  18415  mndind  18863  eqgval  19217  resscntz  19373  frgpuplem  19814  qusabl  19907  dmdprd  20042  dprdcntz2  20082  dprd2d2  20088  isnzr2  20544  chrdvds  21564  chrcong  21565  znleval  21596  isphld  21695  mpfind  22154  gsummoncoe1  22333  pf1ind  22380  smadiadetr  22702  mp2pm2mplem4  22836  isclo  23116  ist1-2  23376  isnrm2  23387  bwth  23439  nconnsubb  23452  subislly  23510  ptclsg  23644  qtopcld  23742  kqcldsat  23762  qustgplem  24150  tsmssubm  24172  ustuqtop  24276  utop2nei  24280  blval2  24596  caucfil  25336  ioorinv  25630  mbfss  25700  iblss2  25861  dvivthlem1  26067  lhop1  26073  deg1leb  26154  reeff1o  26509  sincosq3sgn  26560  sincosq4sgn  26561  dcubic  26907  efrlim  27030  efrlimOLD  27031  fsumharmonic  27073  isppw  27175  issqf  27197  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  ppiub  27266  lgsdinn0  27407  noetainflem4  27803  eqscut  27868  mulsprop  28174  elzs2  28403  elznns  28406  tglngne  28576  tgelrnln  28656  axlowdimlem14  28988  nbgrssovtx  29396  clwwlknclwwlkdif  30011  eupth2lem2  30251  fusgr2wsp2nb  30366  h2hlm  31012  isch2  31255  ch0pss  31477  nmcfnlbi  32084  jplem1  32300  hatomistici  32394  mdsymlem5  32439  cdjreui  32464  dfimafnf  32655  funcnvmpt  32685  fpwrelmap  32747  nn0min  32824  wrdt2ind  32920  swrdrn3  32922  isarchi  33162  zarcls  33820  ordtconnlem1  33870  esumfsup  34034  esumpcvgval  34042  measvuni  34178  aean  34208  eulerpartlemgh  34343  ballotlemsima  34480  sgn3da  34506  bnj1468  34822  subfacp1lem2a  35148  subfacp1lem6  35153  goeleq12bg  35317  dmopab3rexdif  35373  eldm3  35723  onsuct0  36407  bj-equsexvwd  36747  currysetlem1  36913  bj-restsn  37048  ptrest  37579  ptrecube  37580  poimirlem2  37582  poimirlem23  37603  sdclem2  37702  fdc  37705  fdc1  37706  istotbnd3  37731  sstotbnd  37735  prdstotbnd  37754  rrncmslem  37792  brinxprnres  38247  brcnvrabga  38298  alrmomodm  38315  br1cossxrnres  38404  lub0N  39145  glb0N  39149  cdlemefrs29bpre0  40353  dvhb1dimN  40943  dvhopellsm  41074  dibord  41116  dochnel2  41349  mapdvalc  41586  mapdval4N  41589  diophin  42728  diophun  42729  diophrex  42731  3rexfrabdioph  42753  6rexfrabdioph  42755  7rexfrabdioph  42756  zindbi  42903  tfsconcatrn  43304  rababg  43536  relexpnul  43640  clsk1independent  44008  scottabf  44209  hashnzfzclim  44291  fveqsb  44422  infxrbnd2  45284  cncfiooicclem1  45814  stoweidlem35  45956  tz6.12-afv  47088  ndmaovg  47099  tz6.12-afv2  47155  ich2exprop  47345  prprspr2  47392  usgrgrtrirex  47799  line2x  48488  line2y  48489  itsclc0b  48506  clddisj  48583  aacllem  48895