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  4758  elrng  4916  iss  5054  eliniseg  5101  fcnvres  5514  dffv3g  5628  funimass4  5689  fndmdif  5745  fneqeql  5748  funimass3  5756  elrnrexdmb  5780  dff4im  5786  fconst4m  5866  elunirn  5899  riota1  5983  riota2df  5985  f1ocnvfv3  5999  eqfnov  6120  caoftrn  6260  mpoxopovel  6398  rntpos  6414  ordgt0ge1  6594  iinerm  6767  erinxp  6769  qliftfun  6777  mapdm0  6823  elfi2  7155  fifo  7163  inl11  7248  ctssdccl  7294  isomnimap  7320  ismkvmap  7337  iswomnimap  7349  omniwomnimkv  7350  pr2nelem  7380  indpi  7545  genpdflem  7710  genpdisj  7726  genpassl  7727  genpassu  7728  ltnqpri  7797  ltpopr  7798  ltexprlemm  7803  ltexprlemdisj  7809  ltexprlemloc  7810  ltrennb  8057  letri3  8243  letr  8245  ltneg  8625  leneg  8628  reapltxor  8752  apsym  8769  suprnubex  9116  suprleubex  9117  elnnnn0  9428  zrevaddcl  9513  znnsub  9514  znn0sub  9528  prime  9562  eluz2  9744  eluz2b1  9813  nn01to3  9829  qrevaddcl  9856  xrletri3  10017  xrletr  10021  iccid  10138  elicopnf  10182  fzsplit2  10263  fzsn  10279  fzpr  10290  uzsplit  10305  fvinim0ffz  10464  lt2sqi  10866  le2sqi  10867  ccatlcan  11271  ccatrcan  11272  abs00ap  11594  iooinsup  11809  mertenslem2  12068  fprod2dlemstep  12154  gcddiv  12561  algcvgblem  12592  isprm3  12661  dvdsfi  12782  imasmnd2  13506  imasgrp2  13668  issubg  13731  resgrpisgrp  13753  eqgval  13781  imasrng  13940  ring1  14043  imasring  14048  crngunit  14096  lssle0  14357  lssats2  14399  zndvds  14634  znleval  14638  znleval2  14639  eltg2b  14749  discld  14831  opnssneib  14851  restbasg  14863  ssidcn  14905  cnptoprest2  14935  lmss  14941  txrest  14971  txlm  14974  imasnopn  14994  bldisj  15096  xmeter  15131  bl2ioo  15245  limcdifap  15357  bj-sseq  16265  nnti  16469  2omap  16472  pw1nct  16482