Theorem bitr3id 288

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr3g  316  biass  388  imbibiOLD  396  sbcom2  2205  19.16  2259  19.19  2263  necon1bbid  2995  rspc2gv  3590  reuxfr1d  3712  sbceq1a  3754  sbcg  3815  sbcralt  3824  sbccsb2  4401  csbie2df  4407  reuprg0  4667  disjxun  5106  dmopab2rex  5907  dfres3  5983  xp11  6173  ressn  6286  fnssresb  6657  dmfco  6977  funcnvmpt  6991  dffo4  7098  f1ompt  7106  funressn  7156  elunirnALT  7250  fliftf  7313  resoprab2  7529  elrnmpores  7548  ralrnmpo  7549  iunpw  7769  ordunisuc2  7839  tfis  7850  tfinds  7855  dfom2  7863  resf1extb  7930  fiun  7939  f1iun  7940  opiota  8055  1stconst  8094  2ndconst  8095  fnsuppeq0  8187  iinon  8326  dfsmo2  8333  oeeui  8587  omabs  8636  naddrid  8669  brecop  8807  ixpsnf1o  8935  boxcutc  8938  ac6sfi  9243  wemapwe  9665  dmttrcl  9689  scottabf  9865  sdom2en01  10285  ac6num  10462  zorn2lem7  10485  ttukeylem6  10497  alephval2  10556  fpwwe2  10627  fpwwe  10630  nqereu  10913  suplem2pr  11037  map2psrpr  11094  supsrlem  11095  fimaxre3  12160  infm3  12173  crne0  12210  nn1suc  12254  xmulneg1  13294  supxrbnd1  13346  supxrbnd2  13347  iccneg  13498  wrdmap  14582  wrdind  14758  rtrclreclem3  15096  sgn3da  15137  cnpart  15290  sqrt00  15313  lo1resb  15614  o1resb  15616  absefib  16253  efieq1re  16254  sadadd2lem2  16507  saddisjlem  16521  prmind2  16742  isprm7  16766  mreacs  17713  issubc  17891  isfunc  17920  pospo  18398  mndind  18886  eqgval  19244  resscntz  19402  frgpuplem  19841  qusabl  19934  dmdprd  20069  dprdcntz2  20109  dprd2d2  20115  isnzr2  20600  chrdvds  21655  chrcong  21656  znleval  21683  isphld  21783  mpfind  22245  gsummoncoe1  22447  pf1ind  22494  smadiadetr  22811  mp2pm2mplem4  22945  isclo  23223  ist1-2  23483  isnrm2  23494  bwth  23546  nconnsubb  23559  subislly  23617  ptclsg  23751  qtopcld  23849  kqcldsat  23869  qustgplem  24257  tsmssubm  24279  ustuqtop  24382  utop2nei  24386  blval2  24698  caucfil  25421  ioorinv  25714  mbfss  25784  iblss2  25944  dvivthlem1  26146  lhop1  26152  deg1leb  26231  reeff1o  26586  sincosq3sgn  26641  sincosq4sgn  26642  dcubic  26987  efrlim  27110  fsumharmonic  27152  isppw  27254  issqf  27276  fsumdvdsmul  27335  ppiub  27344  lgsdinn0  27485  noetainflem4  27880  eqcuts  27954  mulsprop  28299  elzs2  28568  elznns  28571  tglngne  28795  tgelrnln  28879  tgelrnpln  29032  axlowdimlem14  29271  nbgrssovtx  29677  clwwlknclwwlkdif  30296  eupth2lem2  30536  fusgr2wsp2nb  30651  h2hlm  31298  isch2  31541  ch0pss  31763  nmcfnlbi  32370  jplem1  32586  hatomistici  32680  mdsymlem5  32725  cdjreui  32750  dfimafnf  32947  fpwrelmap  33044  nn0min  33131  wrdt2ind  33239  swrdrn3  33241  gsummptp1  33343  gsummulsubdishift1  33354  isarchi  33468  esplyind  33931  zarcls  34230  ordtconnlem1  34280  esumfsup  34426  esumpcvgval  34434  measvuni  34570  aean  34600  eulerpartlemgh  34734  ballotlemsima  34872  bnj1468  35200  subfacp1lem2a  35626  subfacp1lem6  35631  goeleq12bg  35795  dmopab3rexdif  35851  eldm3  36207  onsuct0  36896  bj-equsexvwd  37342  currysetlem1  37527  bj-restsn  37668  ptrest  38214  ptrecube  38215  poimirlem2  38217  poimirlem23  38238  sdclem2  38337  fdc  38340  fdc1  38341  istotbnd3  38366  sstotbnd  38370  prdstotbnd  38389  rrncmslem  38427  brinxprnres  38892  brcnvrabga  38937  alrmomodm  38954  br1cossxrnres  39133  lub0N  39909  glb0N  39913  cdlemefrs29bpre0  41116  dvhb1dimN  41706  dvhopellsm  41837  dibord  41879  dochnel2  42112  mapdvalc  42349  mapdval4N  42352  diophin  43451  diophun  43452  diophrex  43454  3rexfrabdioph  43472  6rexfrabdioph  43474  7rexfrabdioph  43475  zindbi  43621  tfsconcatrn  44017  rababg  44248  relexpnul  44352  clsk1independent  44720  hashnzfzclim  44980  fveqsb  45109  modelac8prim  45649  infxrbnd2  46032  cncfiooicclem1  46555  stoweidlem35  46697  tz6.12-afv  47855  ndmaovg  47866  tz6.12-afv2  47922  ich2exprop  48165  prprspr2  48212  usgrgrtrirex  48660  line2x  49479  line2y  49480  itsclc0b  49497  reuxfr1dd  49530  clddisj  49627  aacllem  50546