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  2978  sbcel12g  3140  sbceqg  3141  sbcnel12g  3142  reldisj  3544  r19.3rm  3581  eldifpr  3694  eldiftp  3713  rabxp  4761  elrng  4919  iss  5057  eliniseg  5104  fcnvres  5517  dffv3g  5631  funimass4  5692  fndmdif  5748  fneqeql  5751  funimass3  5759  elrnrexdmb  5783  dff4im  5789  fconst4m  5869  elunirn  5902  riota1  5986  riota2df  5988  f1ocnvfv3  6002  eqfnov  6123  caoftrn  6263  mpoxopovel  6402  rntpos  6418  ordgt0ge1  6598  iinerm  6771  erinxp  6773  qliftfun  6781  mapdm0  6827  elfi2  7165  fifo  7173  inl11  7258  ctssdccl  7304  isomnimap  7330  ismkvmap  7347  iswomnimap  7359  omniwomnimkv  7360  pr2nelem  7390  indpi  7555  genpdflem  7720  genpdisj  7736  genpassl  7737  genpassu  7738  ltnqpri  7807  ltpopr  7808  ltexprlemm  7813  ltexprlemdisj  7819  ltexprlemloc  7820  ltrennb  8067  letri3  8253  letr  8255  ltneg  8635  leneg  8638  reapltxor  8762  apsym  8779  suprnubex  9126  suprleubex  9127  elnnnn0  9438  zrevaddcl  9523  znnsub  9524  znn0sub  9538  prime  9572  eluz2  9754  eluz2b1  9828  nn01to3  9844  qrevaddcl  9871  xrletri3  10032  xrletr  10036  iccid  10153  elicopnf  10197  fzsplit2  10278  fzsn  10294  fzpr  10305  uzsplit  10320  fvinim0ffz  10480  lt2sqi  10882  le2sqi  10883  ccatlcan  11292  ccatrcan  11293  abs00ap  11616  iooinsup  11831  mertenslem2  12090  fprod2dlemstep  12176  gcddiv  12583  algcvgblem  12614  isprm3  12683  dvdsfi  12804  imasmnd2  13528  imasgrp2  13690  issubg  13753  resgrpisgrp  13775  eqgval  13803  imasrng  13962  ring1  14065  imasring  14070  crngunit  14118  lssle0  14379  lssats2  14421  zndvds  14656  znleval  14660  znleval2  14661  eltg2b  14771  discld  14853  opnssneib  14873  restbasg  14885  ssidcn  14927  cnptoprest2  14957  lmss  14963  txrest  14993  txlm  14996  imasnopn  15016  bldisj  15118  xmeter  15153  bl2ioo  15267  limcdifap  15379  bj-sseq  16338  nnti  16541  2omap  16544  pw1nct  16554