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  3bior1fd  1364  3biant1d  1367  equsalh  1750  eueq3dc  2948  sbcel12g  3109  sbceqg  3110  sbcnel12g  3111  reldisj  3513  r19.3rm  3550  eldifpr  3661  eldiftp  3680  rabxp  4716  elrng  4873  iss  5010  eliniseg  5057  fcnvres  5466  dffv3g  5579  funimass4  5636  fndmdif  5692  fneqeql  5695  funimass3  5703  elrnrexdmb  5727  dff4im  5733  fconst4m  5811  elunirn  5842  riota1  5925  riota2df  5927  f1ocnvfv3  5940  eqfnov  6059  caoftrn  6198  mpoxopovel  6334  rntpos  6350  ordgt0ge1  6528  iinerm  6701  erinxp  6703  qliftfun  6711  mapdm0  6757  elfi2  7081  fifo  7089  inl11  7174  ctssdccl  7220  isomnimap  7246  ismkvmap  7263  iswomnimap  7275  omniwomnimkv  7276  pr2nelem  7306  indpi  7462  genpdflem  7627  genpdisj  7643  genpassl  7644  genpassu  7645  ltnqpri  7714  ltpopr  7715  ltexprlemm  7720  ltexprlemdisj  7726  ltexprlemloc  7727  ltrennb  7974  letri3  8160  letr  8162  ltneg  8542  leneg  8545  reapltxor  8669  apsym  8686  suprnubex  9033  suprleubex  9034  elnnnn0  9345  zrevaddcl  9430  znnsub  9431  znn0sub  9445  prime  9479  eluz2  9661  eluz2b1  9729  nn01to3  9745  qrevaddcl  9772  xrletri3  9933  xrletr  9937  iccid  10054  elicopnf  10098  fzsplit2  10179  fzsn  10195  fzpr  10206  uzsplit  10221  fvinim0ffz  10377  lt2sqi  10779  le2sqi  10780  abs00ap  11417  iooinsup  11632  mertenslem2  11891  fprod2dlemstep  11977  gcddiv  12384  algcvgblem  12415  isprm3  12484  dvdsfi  12605  imasmnd2  13328  imasgrp2  13490  issubg  13553  resgrpisgrp  13575  eqgval  13603  imasrng  13762  ring1  13865  imasring  13870  crngunit  13917  lssle0  14178  lssats2  14220  zndvds  14455  znleval  14459  znleval2  14460  eltg2b  14570  discld  14652  opnssneib  14672  restbasg  14684  ssidcn  14726  cnptoprest2  14756  lmss  14762  txrest  14792  txlm  14795  imasnopn  14815  bldisj  14917  xmeter  14952  bl2ioo  15066  limcdifap  15178  bj-sseq  15802  nnti  16003  2omap  16006  pw1nct  16014