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  1366  3biant1d  1369  equsalh  1752  eueq3dc  2957  sbcel12g  3119  sbceqg  3120  sbcnel12g  3121  reldisj  3523  r19.3rm  3560  eldifpr  3673  eldiftp  3692  rabxp  4733  elrng  4890  iss  5027  eliniseg  5074  fcnvres  5485  dffv3g  5599  funimass4  5657  fndmdif  5713  fneqeql  5716  funimass3  5724  elrnrexdmb  5748  dff4im  5754  fconst4m  5832  elunirn  5863  riota1  5947  riota2df  5949  f1ocnvfv3  5963  eqfnov  6082  caoftrn  6221  mpoxopovel  6357  rntpos  6373  ordgt0ge1  6551  iinerm  6724  erinxp  6726  qliftfun  6734  mapdm0  6780  elfi2  7107  fifo  7115  inl11  7200  ctssdccl  7246  isomnimap  7272  ismkvmap  7289  iswomnimap  7301  omniwomnimkv  7302  pr2nelem  7332  indpi  7497  genpdflem  7662  genpdisj  7678  genpassl  7679  genpassu  7680  ltnqpri  7749  ltpopr  7750  ltexprlemm  7755  ltexprlemdisj  7761  ltexprlemloc  7762  ltrennb  8009  letri3  8195  letr  8197  ltneg  8577  leneg  8580  reapltxor  8704  apsym  8721  suprnubex  9068  suprleubex  9069  elnnnn0  9380  zrevaddcl  9465  znnsub  9466  znn0sub  9480  prime  9514  eluz2  9696  eluz2b1  9764  nn01to3  9780  qrevaddcl  9807  xrletri3  9968  xrletr  9972  iccid  10089  elicopnf  10133  fzsplit2  10214  fzsn  10230  fzpr  10241  uzsplit  10256  fvinim0ffz  10414  lt2sqi  10816  le2sqi  10817  ccatlcan  11216  ccatrcan  11217  abs00ap  11539  iooinsup  11754  mertenslem2  12013  fprod2dlemstep  12099  gcddiv  12506  algcvgblem  12537  isprm3  12606  dvdsfi  12727  imasmnd2  13451  imasgrp2  13613  issubg  13676  resgrpisgrp  13698  eqgval  13726  imasrng  13885  ring1  13988  imasring  13993  crngunit  14040  lssle0  14301  lssats2  14343  zndvds  14578  znleval  14582  znleval2  14583  eltg2b  14693  discld  14775  opnssneib  14795  restbasg  14807  ssidcn  14849  cnptoprest2  14879  lmss  14885  txrest  14915  txlm  14918  imasnopn  14938  bldisj  15040  xmeter  15075  bl2ioo  15189  limcdifap  15301  bj-sseq  16066  nnti  16267  2omap  16270  pw1nct  16280