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  2172  19.16  2224  19.19  2228  necon1bbid  2979  rspc2gv  3631  reuxfr1d  3755  sbceq1a  3798  sbcg  3862  sbcralt  3871  sbccsb2  4436  csbie2df  4442  reuprg0  4701  disjxun  5140  dmopab2rex  5927  dfres3  6001  xp11  6194  ressn  6304  fnssresb  6689  dmfco  7004  dffo4  7122  f1ompt  7130  funressn  7178  elunirnALT  7273  fliftf  7336  resoprab2  7553  elrnmpores  7572  ralrnmpo  7573  iunpw  7792  ordunisuc2  7866  tfis  7877  tfinds  7882  dfom2  7890  resf1extb  7957  fiun  7968  f1iun  7969  opiota  8085  1stconst  8126  2ndconst  8127  fnsuppeq0  8218  iinon  8381  dfsmo2  8388  oeeui  8641  omabs  8690  naddrid  8722  brecop  8851  ixpsnf1o  8979  boxcutc  8982  ac6sfi  9321  wemapwe  9738  dmttrcl  9762  sdom2en01  10343  ac6num  10520  zorn2lem7  10543  ttukeylem6  10555  alephval2  10613  fpwwe2  10684  fpwwe  10687  nqereu  10970  suplem2pr  11094  map2psrpr  11151  supsrlem  11152  fimaxre3  12215  infm3  12228  crne0  12260  nn1suc  12289  xmulneg1  13312  supxrbnd1  13364  supxrbnd2  13365  iccneg  13513  wrdmap  14585  wrdind  14761  rtrclreclem3  15100  cnpart  15280  sqrt00  15303  lo1resb  15601  o1resb  15603  absefib  16235  efieq1re  16236  sadadd2lem2  16488  saddisjlem  16502  prmind2  16723  isprm7  16746  mreacs  17702  issubc  17881  isfunc  17910  pospo  18391  mndind  18842  eqgval  19196  resscntz  19352  frgpuplem  19791  qusabl  19884  dmdprd  20019  dprdcntz2  20059  dprd2d2  20065  isnzr2  20519  chrdvds  21542  chrcong  21543  znleval  21574  isphld  21673  mpfind  22132  gsummoncoe1  22313  pf1ind  22360  smadiadetr  22682  mp2pm2mplem4  22816  isclo  23096  ist1-2  23356  isnrm2  23367  bwth  23419  nconnsubb  23432  subislly  23490  ptclsg  23624  qtopcld  23722  kqcldsat  23742  qustgplem  24130  tsmssubm  24152  ustuqtop  24256  utop2nei  24260  blval2  24576  caucfil  25318  ioorinv  25612  mbfss  25682  iblss2  25842  dvivthlem1  26048  lhop1  26054  deg1leb  26135  reeff1o  26492  sincosq3sgn  26543  sincosq4sgn  26544  dcubic  26890  efrlim  27013  efrlimOLD  27014  fsumharmonic  27056  isppw  27158  issqf  27180  fsumdvdsmul  27239  fsumdvdsmulOLD  27241  ppiub  27249  lgsdinn0  27390  noetainflem4  27786  eqscut  27851  mulsprop  28157  elzs2  28386  elznns  28389  tglngne  28559  tgelrnln  28639  axlowdimlem14  28971  nbgrssovtx  29379  clwwlknclwwlkdif  29999  eupth2lem2  30239  fusgr2wsp2nb  30354  h2hlm  31000  isch2  31243  ch0pss  31465  nmcfnlbi  32072  jplem1  32288  hatomistici  32382  mdsymlem5  32427  cdjreui  32452  dfimafnf  32647  funcnvmpt  32678  fpwrelmap  32745  nn0min  32823  wrdt2ind  32939  swrdrn3  32941  isarchi  33190  zarcls  33874  ordtconnlem1  33924  esumfsup  34072  esumpcvgval  34080  measvuni  34216  aean  34246  eulerpartlemgh  34381  ballotlemsima  34519  sgn3da  34545  bnj1468  34861  subfacp1lem2a  35186  subfacp1lem6  35191  goeleq12bg  35355  dmopab3rexdif  35411  eldm3  35762  onsuct0  36443  bj-equsexvwd  36783  currysetlem1  36949  bj-restsn  37084  ptrest  37627  ptrecube  37628  poimirlem2  37630  poimirlem23  37651  sdclem2  37750  fdc  37753  fdc1  37754  istotbnd3  37779  sstotbnd  37783  prdstotbnd  37802  rrncmslem  37840  brinxprnres  38293  brcnvrabga  38344  alrmomodm  38361  br1cossxrnres  38450  lub0N  39191  glb0N  39195  cdlemefrs29bpre0  40399  dvhb1dimN  40989  dvhopellsm  41120  dibord  41162  dochnel2  41395  mapdvalc  41632  mapdval4N  41635  diophin  42788  diophun  42789  diophrex  42791  3rexfrabdioph  42813  6rexfrabdioph  42815  7rexfrabdioph  42816  zindbi  42963  tfsconcatrn  43360  rababg  43592  relexpnul  43696  clsk1independent  44064  scottabf  44264  hashnzfzclim  44346  fveqsb  44477  modelac8prim  45014  infxrbnd2  45385  cncfiooicclem1  45913  stoweidlem35  46055  tz6.12-afv  47190  ndmaovg  47201  tz6.12-afv2  47257  ich2exprop  47463  prprspr2  47510  usgrgrtrirex  47922  line2x  48680  line2y  48681  itsclc0b  48698  reuxfr1dd  48731  clddisj  48808  aacllem  49375