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  3575  reuxfr1d  3697  sbceq1a  3740  sbcg  3802  sbcralt  3811  sbccsb2  4378  csbie2df  4384  reuprg0  4647  disjxun  5084  dmopab2rex  5864  dfres3  5941  xp11  6131  ressn  6241  fnssresb  6612  dmfco  6928  funcnvmpt  6941  dffo4  7047  f1ompt  7055  funressn  7104  elunirnALT  7198  fliftf  7261  resoprab2  7477  elrnmpores  7496  ralrnmpo  7497  iunpw  7716  ordunisuc2  7786  tfis  7797  tfinds  7802  dfom2  7810  resf1extb  7876  fiun  7887  f1iun  7888  opiota  8003  1stconst  8041  2ndconst  8042  fnsuppeq0  8133  iinon  8271  dfsmo2  8278  oeeui  8529  omabs  8578  naddrid  8610  brecop  8748  ixpsnf1o  8877  boxcutc  8880  ac6sfi  9185  wemapwe  9607  dmttrcl  9631  sdom2en01  10213  ac6num  10390  zorn2lem7  10413  ttukeylem6  10425  alephval2  10484  fpwwe2  10555  fpwwe  10558  nqereu  10841  suplem2pr  10965  map2psrpr  11022  supsrlem  11023  fimaxre3  12089  infm3  12102  crne0  12139  nn1suc  12168  xmulneg1  13185  supxrbnd1  13237  supxrbnd2  13238  iccneg  13389  wrdmap  14470  wrdind  14646  rtrclreclem3  14984  cnpart  15164  sqrt00  15187  lo1resb  15488  o1resb  15490  absefib  16124  efieq1re  16125  sadadd2lem2  16378  saddisjlem  16392  prmind2  16613  isprm7  16636  mreacs  17582  issubc  17760  isfunc  17789  pospo  18267  mndind  18754  eqgval  19110  resscntz  19266  frgpuplem  19705  qusabl  19798  dmdprd  19933  dprdcntz2  19973  dprd2d2  19979  isnzr2  20453  chrdvds  21483  chrcong  21484  znleval  21511  isphld  21611  mpfind  22071  gsummoncoe1  22251  pf1ind  22298  smadiadetr  22618  mp2pm2mplem4  22752  isclo  23030  ist1-2  23290  isnrm2  23301  bwth  23353  nconnsubb  23366  subislly  23424  ptclsg  23558  qtopcld  23656  kqcldsat  23676  qustgplem  24064  tsmssubm  24086  ustuqtop  24189  utop2nei  24193  blval2  24505  caucfil  25228  ioorinv  25521  mbfss  25591  iblss2  25751  dvivthlem1  25954  lhop1  25960  deg1leb  26041  reeff1o  26397  sincosq3sgn  26449  sincosq4sgn  26450  dcubic  26796  efrlim  26919  efrlimOLD  26920  fsumharmonic  26962  isppw  27064  issqf  27086  fsumdvdsmul  27145  fsumdvdsmulOLD  27147  ppiub  27155  lgsdinn0  27296  noetainflem4  27692  eqcuts  27765  mulsprop  28110  elzs2  28379  elznns  28382  tglngne  28606  tgelrnln  28686  axlowdimlem14  29012  nbgrssovtx  29418  clwwlknclwwlkdif  30038  eupth2lem2  30278  fusgr2wsp2nb  30393  h2hlm  31040  isch2  31283  ch0pss  31505  nmcfnlbi  32112  jplem1  32328  hatomistici  32422  mdsymlem5  32467  cdjreui  32492  dfimafnf  32698  fpwrelmap  32795  nn0min  32884  sgn3da  32898  wrdt2ind  33018  swrdrn3  33020  gsummptp1  33123  gsummulsubdishift1  33134  isarchi  33248  esplyind  33724  zarcls  34024  ordtconnlem1  34074  esumfsup  34220  esumpcvgval  34228  measvuni  34364  aean  34394  eulerpartlemgh  34528  ballotlemsima  34666  bnj1468  34994  subfacp1lem2a  35368  subfacp1lem6  35373  goeleq12bg  35537  dmopab3rexdif  35593  eldm3  35949  onsuct0  36629  bj-equsexvwd  37068  currysetlem1  37252  bj-restsn  37392  ptrest  37931  ptrecube  37932  poimirlem2  37934  poimirlem23  37955  sdclem2  38054  fdc  38057  fdc1  38058  istotbnd3  38083  sstotbnd  38087  prdstotbnd  38106  rrncmslem  38144  brinxprnres  38609  brcnvrabga  38654  alrmomodm  38671  br1cossxrnres  38850  lub0N  39626  glb0N  39630  cdlemefrs29bpre0  40833  dvhb1dimN  41423  dvhopellsm  41554  dibord  41596  dochnel2  41829  mapdvalc  42066  mapdval4N  42069  diophin  43203  diophun  43204  diophrex  43206  3rexfrabdioph  43228  6rexfrabdioph  43230  7rexfrabdioph  43231  zindbi  43377  tfsconcatrn  43773  rababg  44004  relexpnul  44108  clsk1independent  44476  scottabf  44670  hashnzfzclim  44752  fveqsb  44882  modelac8prim  45422  infxrbnd2  45801  cncfiooicclem1  46325  stoweidlem35  46467  tz6.12-afv  47607  ndmaovg  47618  tz6.12-afv2  47674  ich2exprop  47905  prprspr2  47952  usgrgrtrirex  48384  line2x  49188  line2y  49189  itsclc0b  49206  reuxfr1dd  49240  clddisj  49337  aacllem  50234