Theorem bitr4di 198

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4di.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
bitr4di	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 132	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 196	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr4g  223  bibi2i  227  equsalh  1737  eueq3dc  2935  sbcel12g  3096  sbceqg  3097  sbcnel12g  3098  reldisj  3499  r19.3rm  3536  eldifpr  3646  eldiftp  3665  rabxp  4697  elrng  4854  iss  4989  eliniseg  5036  fcnvres  5438  dffv3g  5551  funimass4  5608  fndmdif  5664  fneqeql  5667  funimass3  5675  elrnrexdmb  5699  dff4im  5705  fconst4m  5779  elunirn  5810  riota1  5893  riota2df  5895  f1ocnvfv3  5908  eqfnov  6026  caoftrn  6160  mpoxopovel  6296  rntpos  6312  ordgt0ge1  6490  iinerm  6663  erinxp  6665  qliftfun  6673  mapdm0  6719  elfi2  7033  fifo  7041  inl11  7126  ctssdccl  7172  isomnimap  7198  ismkvmap  7215  iswomnimap  7227  omniwomnimkv  7228  pr2nelem  7253  indpi  7404  genpdflem  7569  genpdisj  7585  genpassl  7586  genpassu  7587  ltnqpri  7656  ltpopr  7657  ltexprlemm  7662  ltexprlemdisj  7668  ltexprlemloc  7669  ltrennb  7916  letri3  8102  letr  8104  ltneg  8483  leneg  8486  reapltxor  8610  apsym  8627  suprnubex  8974  suprleubex  8975  elnnnn0  9286  zrevaddcl  9370  znnsub  9371  znn0sub  9385  prime  9419  eluz2  9601  eluz2b1  9669  nn01to3  9685  qrevaddcl  9712  xrletri3  9873  xrletr  9877  iccid  9994  elicopnf  10038  fzsplit2  10119  fzsn  10135  fzpr  10146  uzsplit  10161  fvinim0ffz  10311  lt2sqi  10701  le2sqi  10702  abs00ap  11209  iooinsup  11423  mertenslem2  11682  fprod2dlemstep  11768  gcddiv  12159  algcvgblem  12190  isprm3  12259  phisum  12381  imasgrp2  13183  issubg  13246  resgrpisgrp  13268  eqgval  13296  imasrng  13455  ring1  13558  imasring  13563  crngunit  13610  lssle0  13871  lssats2  13913  zndvds  14148  znleval  14152  znleval2  14153  eltg2b  14233  discld  14315  opnssneib  14335  restbasg  14347  ssidcn  14389  cnptoprest2  14419  lmss  14425  txrest  14455  txlm  14458  imasnopn  14478  bldisj  14580  xmeter  14615  bl2ioo  14729  limcdifap  14841  bj-sseq  15354  nnti  15555  pw1nct  15563