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 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr3g  316  biass  388  imbibiOLD  397  sbcom2  2212  19.16  2265  19.19  2269  necon1bbid  2998  rspc2gv  3589  reuxfr1d  3711  sbceq1a  3753  sbcg  3814  sbcralt  3823  sbccsb2  4398  csbie2df  4404  reuprg0  4663  disjxun  5104  dmopab2rex  5906  dfres3  5986  xp11  6179  ressn  6306  fnssresb  6683  dmfco  7004  funcnvmpt  7018  dffo4  7127  f1ompt  7135  funressn  7187  elunirnALT  7279  fliftf  7346  resoprab2  7562  elrnmpores  7582  ralrnmpo  7583  iunpw  7809  ordunisuc2  7879  tfis  7890  tfinds  7895  dfom2  7903  resf1extb  7970  fiun  7979  f1iun  7980  opiota  8095  1stconst  8138  2ndconst  8139  fnsuppeq0  8237  iinon  8376  dfsmo2  8383  oeeui  8639  omabs  8688  naddrid  8721  brecop  8859  ixpsnf1o  8994  boxcutc  8997  ac6sfi  9303  wemapwe  9725  dmttrcl  9749  scottabf  9966  sdom2en01  10407  ac6num  10584  zorn2lem7  10607  ttukeylem6  10619  alephval2  10684  fpwwe2  10755  fpwwe  10758  nqereu  11041  suplem2pr  11165  map2psrpr  11222  supsrlem  11223  fimaxre3  12290  infm3  12303  crne0  12340  nn1suc  12384  xmulneg1  13426  supxrbnd1  13478  supxrbnd2  13479  iccneg  13630  wrdmap  14718  swrdrn3  14830  wrdind  14899  rtrclreclem3  15242  sgn3da  15283  cnpart  15436  sqrt00  15459  lo1resb  15760  o1resb  15762  absefib  16395  efieq1re  16396  sadadd2lem2  16649  saddisjlem  16663  prmind2  16889  isprm7  16913  mreacs  17861  issubc  18039  isfunc  18068  pospo  18546  mndind  19053  eqgval  19418  resscntz  19577  frgpuplem  20016  qusabl  20109  dmdprd  20244  dprdcntz2  20284  dprd2d2  20290  isnzr2  20798  chrdvds  21862  chrcong  21863  znleval  21890  isphld  21990  mpfind  22454  gsummoncoe1  22656  pf1ind  22703  smadiadetr  23020  mp2pm2mplem4  23157  isclo  23435  ist1-2  23695  isnrm2  23706  bwth  23758  nconnsubb  23771  subislly  23830  ptclsg  23964  qtopcld  24062  kqcldsat  24082  qustgplem  24470  tsmssubm  24492  ustuqtop  24595  utop2nei  24599  blval2  24911  caucfil  25634  ioorinv  25927  mbfss  25997  iblss2  26156  dvivthlem1  26358  lhop1  26364  deg1leb  26443  reeff1o  26804  sincosq3sgn  26859  sincosq4sgn  26860  dcubic  27204  efrlim  27327  fsumharmonic  27369  isppw  27471  issqf  27493  fsumdvdsmul  27552  ppiub  27561  lgsdinn0  27702  noetainflem4  28127  eqcuts  28201  mulsprop  28546  elzs2  28815  elznns  28818  tglngne  29043  tgelrnln  29128  tgelrnpln  29284  axlowdimlem14  29563  nbgrssovtx  29972  clwwlknclwwlkdif  30600  eupth2lem2  30850  fusgr2wsp2nb  30965  h2hlm  31612  isch2  31855  ch0pss  32077  nmcfnlbi  32684  jplem1  32900  hatomistici  32994  mdsymlem5  33039  cdjreui  33064  dfimafnf  33302  fpwrelmap  33395  nn0min  33482  wrdt2ind  33586  gsummptp1  33688  gsummulsubdishift1  33699  isarchi  33813  esplyind  34277  zarcls  34576  ordtconnlem1  34626  esumfsup  34772  esumpcvgval  34780  measvuni  34917  aean  34947  eulerpartlemgh  35080  ballotlemsima  35218  bnj1468  35546  fwfffun  35787  j00smo  36005  subfacp1lem2a  36112  subfacp1lem6  36117  goeleq12bg  36281  dmopab3rexdif  36337  eldm3  36704  onsuct0  37407  bj-equsexvwd  37853  currysetlem1  38038  bj-restsn  38194  ptrest  38729  ptrecube  38730  poimirlem2  38732  poimirlem23  38753  sdclem2  38868  fdc  38871  fdc1  38872  istotbnd3  38897  sstotbnd  38901  prdstotbnd  38920  rrncmslem  38958  brinxprnres  39421  brcnvrabga  39466  alrmomodm  39483  br1cossxrnres  39662  lub0N  40438  glb0N  40442  cdlemefrs29bpre0  41645  dvhb1dimN  42235  dvhopellsm  42366  dibord  42408  dochnel2  42641  mapdvalc  42878  mapdval4N  42881  diophin  43976  diophun  43977  diophrex  43979  3rexfrabdioph  43997  6rexfrabdioph  43999  7rexfrabdioph  44000  zindbi  44146  tfsconcatrn  44536  rababg  44767  relexpnul  44870  clsk1independent  45238  hashnzfzclim  45498  fveqsb  45626  modelac8prim  46177  infxrbnd2  46585  cncfiooicclem1  47108  stoweidlem35  47250  tz6.12-afv  48448  ndmaovg  48459  tz6.12-afv2  48515  ich2exprop  48758  prprspr2  48805  usgrgrtrirex  49253  line2x  50071  line2y  50072  itsclc0b  50089  reuxfr1dd  50122  clddisj  50223  aacllem  51219