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  5873  dfres3  5950  xp11  6140  ressn  6250  fnssresb  6621  dmfco  6937  funcnvmpt  6950  dffo4  7056  f1ompt  7064  funressn  7113  elunirnALT  7207  fliftf  7270  resoprab2  7486  elrnmpores  7505  ralrnmpo  7506  iunpw  7725  ordunisuc2  7795  tfis  7806  tfinds  7811  dfom2  7819  resf1extb  7885  fiun  7896  f1iun  7897  opiota  8012  1stconst  8050  2ndconst  8051  fnsuppeq0  8142  iinon  8280  dfsmo2  8287  oeeui  8538  omabs  8587  naddrid  8619  brecop  8757  ixpsnf1o  8886  boxcutc  8889  ac6sfi  9194  wemapwe  9618  dmttrcl  9642  sdom2en01  10224  ac6num  10401  zorn2lem7  10424  ttukeylem6  10436  alephval2  10495  fpwwe2  10566  fpwwe  10569  nqereu  10852  suplem2pr  10976  map2psrpr  11033  supsrlem  11034  fimaxre3  12102  infm3  12115  crne0  12152  nn1suc  12196  xmulneg1  13221  supxrbnd1  13273  supxrbnd2  13274  iccneg  13425  wrdmap  14508  wrdind  14684  rtrclreclem3  15022  cnpart  15202  sqrt00  15225  lo1resb  15526  o1resb  15528  absefib  16165  efieq1re  16166  sadadd2lem2  16419  saddisjlem  16433  prmind2  16654  isprm7  16678  mreacs  17624  issubc  17802  isfunc  17831  pospo  18309  mndind  18796  eqgval  19152  resscntz  19308  frgpuplem  19747  qusabl  19840  dmdprd  19975  dprdcntz2  20015  dprd2d2  20021  isnzr2  20495  chrdvds  21506  chrcong  21507  znleval  21534  isphld  21634  mpfind  22093  gsummoncoe1  22273  pf1ind  22320  smadiadetr  22640  mp2pm2mplem4  22774  isclo  23052  ist1-2  23312  isnrm2  23323  bwth  23375  nconnsubb  23388  subislly  23446  ptclsg  23580  qtopcld  23678  kqcldsat  23698  qustgplem  24086  tsmssubm  24108  ustuqtop  24211  utop2nei  24215  blval2  24527  caucfil  25250  ioorinv  25543  mbfss  25613  iblss2  25773  dvivthlem1  25975  lhop1  25981  deg1leb  26060  reeff1o  26412  sincosq3sgn  26464  sincosq4sgn  26465  dcubic  26810  efrlim  26933  fsumharmonic  26975  isppw  27077  issqf  27099  fsumdvdsmul  27158  ppiub  27167  lgsdinn0  27308  noetainflem4  27704  eqcuts  27777  mulsprop  28122  elzs2  28391  elznns  28394  tglngne  28618  tgelrnln  28698  axlowdimlem14  29024  nbgrssovtx  29430  clwwlknclwwlkdif  30049  eupth2lem2  30289  fusgr2wsp2nb  30404  h2hlm  31051  isch2  31294  ch0pss  31516  nmcfnlbi  32123  jplem1  32339  hatomistici  32433  mdsymlem5  32478  cdjreui  32503  dfimafnf  32709  fpwrelmap  32806  nn0min  32894  sgn3da  32907  wrdt2ind  33013  swrdrn3  33015  gsummptp1  33118  gsummulsubdishift1  33129  isarchi  33243  esplyind  33719  zarcls  34018  ordtconnlem1  34068  esumfsup  34214  esumpcvgval  34222  measvuni  34358  aean  34388  eulerpartlemgh  34522  ballotlemsima  34660  bnj1468  34988  subfacp1lem2a  35362  subfacp1lem6  35367  goeleq12bg  35531  dmopab3rexdif  35587  eldm3  35943  onsuct0  36623  bj-equsexvwd  37070  currysetlem1  37254  bj-restsn  37394  ptrest  37940  ptrecube  37941  poimirlem2  37943  poimirlem23  37964  sdclem2  38063  fdc  38066  fdc1  38067  istotbnd3  38092  sstotbnd  38096  prdstotbnd  38115  rrncmslem  38153  brinxprnres  38618  brcnvrabga  38663  alrmomodm  38680  br1cossxrnres  38859  lub0N  39635  glb0N  39639  cdlemefrs29bpre0  40842  dvhb1dimN  41432  dvhopellsm  41563  dibord  41605  dochnel2  41838  mapdvalc  42075  mapdval4N  42078  diophin  43204  diophun  43205  diophrex  43207  3rexfrabdioph  43225  6rexfrabdioph  43227  7rexfrabdioph  43228  zindbi  43374  tfsconcatrn  43770  rababg  44001  relexpnul  44105  clsk1independent  44473  scottabf  44667  hashnzfzclim  44749  fveqsb  44879  modelac8prim  45419  infxrbnd2  45798  cncfiooicclem1  46321  stoweidlem35  46463  tz6.12-afv  47615  ndmaovg  47626  tz6.12-afv2  47682  ich2exprop  47925  prprspr2  47972  usgrgrtrirex  48420  line2x  49224  line2y  49225  itsclc0b  49242  reuxfr1dd  49276  clddisj  49373  aacllem  50270