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  1386  3biant1d  1389  equsalh  1772  eueq3dc  2977  sbcel12g  3139  sbceqg  3140  sbcnel12g  3141  reldisj  3543  r19.3rm  3580  eldifpr  3693  eldiftp  3712  rabxp  4756  elrng  4913  iss  5051  eliniseg  5098  fcnvres  5509  dffv3g  5623  funimass4  5684  fndmdif  5740  fneqeql  5743  funimass3  5751  elrnrexdmb  5775  dff4im  5781  fconst4m  5859  elunirn  5890  riota1  5974  riota2df  5976  f1ocnvfv3  5990  eqfnov  6111  caoftrn  6251  mpoxopovel  6387  rntpos  6403  ordgt0ge1  6581  iinerm  6754  erinxp  6756  qliftfun  6764  mapdm0  6810  elfi2  7139  fifo  7147  inl11  7232  ctssdccl  7278  isomnimap  7304  ismkvmap  7321  iswomnimap  7333  omniwomnimkv  7334  pr2nelem  7364  indpi  7529  genpdflem  7694  genpdisj  7710  genpassl  7711  genpassu  7712  ltnqpri  7781  ltpopr  7782  ltexprlemm  7787  ltexprlemdisj  7793  ltexprlemloc  7794  ltrennb  8041  letri3  8227  letr  8229  ltneg  8609  leneg  8612  reapltxor  8736  apsym  8753  suprnubex  9100  suprleubex  9101  elnnnn0  9412  zrevaddcl  9497  znnsub  9498  znn0sub  9512  prime  9546  eluz2  9728  eluz2b1  9796  nn01to3  9812  qrevaddcl  9839  xrletri3  10000  xrletr  10004  iccid  10121  elicopnf  10165  fzsplit2  10246  fzsn  10262  fzpr  10273  uzsplit  10288  fvinim0ffz  10447  lt2sqi  10849  le2sqi  10850  ccatlcan  11250  ccatrcan  11251  abs00ap  11573  iooinsup  11788  mertenslem2  12047  fprod2dlemstep  12133  gcddiv  12540  algcvgblem  12571  isprm3  12640  dvdsfi  12761  imasmnd2  13485  imasgrp2  13647  issubg  13710  resgrpisgrp  13732  eqgval  13760  imasrng  13919  ring1  14022  imasring  14027  crngunit  14075  lssle0  14336  lssats2  14378  zndvds  14613  znleval  14617  znleval2  14618  eltg2b  14728  discld  14810  opnssneib  14830  restbasg  14842  ssidcn  14884  cnptoprest2  14914  lmss  14920  txrest  14950  txlm  14953  imasnopn  14973  bldisj  15075  xmeter  15110  bl2ioo  15224  limcdifap  15336  bj-sseq  16156  nnti  16356  2omap  16359  pw1nct  16369