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  1726  eueq3dc  2913  sbcel12g  3074  sbceqg  3075  sbcnel12g  3076  reldisj  3476  r19.3rm  3513  eldifpr  3621  eldiftp  3640  rabxp  4665  elrng  4820  iss  4955  eliniseg  5000  fcnvres  5401  dffv3g  5513  funimass4  5568  fndmdif  5623  fneqeql  5626  funimass3  5634  elrnrexdmb  5658  dff4im  5664  fconst4m  5738  elunirn  5769  riota1  5851  riota2df  5853  f1ocnvfv3  5866  eqfnov  5983  caoftrn  6110  mpoxopovel  6244  rntpos  6260  ordgt0ge1  6438  iinerm  6609  erinxp  6611  qliftfun  6619  mapdm0  6665  elfi2  6973  fifo  6981  inl11  7066  ctssdccl  7112  isomnimap  7137  ismkvmap  7154  iswomnimap  7166  omniwomnimkv  7167  pr2nelem  7192  indpi  7343  genpdflem  7508  genpdisj  7524  genpassl  7525  genpassu  7526  ltnqpri  7595  ltpopr  7596  ltexprlemm  7601  ltexprlemdisj  7607  ltexprlemloc  7608  ltrennb  7855  letri3  8040  letr  8042  ltneg  8421  leneg  8424  reapltxor  8548  apsym  8565  suprnubex  8912  suprleubex  8913  elnnnn0  9221  zrevaddcl  9305  znnsub  9306  znn0sub  9320  prime  9354  eluz2  9536  eluz2b1  9603  nn01to3  9619  qrevaddcl  9646  xrletri3  9806  xrletr  9810  iccid  9927  elicopnf  9971  fzsplit2  10052  fzsn  10068  fzpr  10079  uzsplit  10094  fvinim0ffz  10243  lt2sqi  10610  le2sqi  10611  abs00ap  11073  iooinsup  11287  mertenslem2  11546  fprod2dlemstep  11632  gcddiv  12022  algcvgblem  12051  isprm3  12120  phisum  12242  issubg  13038  resgrpisgrp  13060  eqgval  13087  ring1  13241  crngunit  13285  lssle0  13463  eltg2b  13593  discld  13675  opnssneib  13695  restbasg  13707  ssidcn  13749  cnptoprest2  13779  lmss  13785  txrest  13815  txlm  13818  imasnopn  13838  bldisj  13940  xmeter  13975  bl2ioo  14081  limcdifap  14170  bj-sseq  14583  nnti  14783  pw1nct  14791