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  1389  3biant1d  1392  equsalh  1774  eueq3dc  2994  sbcel12g  3156  sbceqg  3157  sbcnel12g  3158  reldisj  3564  r19.3rm  3602  eldifpr  3721  eldiftp  3740  rabxp  4792  elrng  4951  iss  5089  eliniseg  5137  fcnvres  5555  dffv3g  5671  funimass4  5732  fndmdif  5788  fneqeql  5791  funimass3  5799  elrnrexdmb  5822  dff4im  5828  fconst4m  5909  elunirn  5945  riota1  6031  riota2df  6033  f1ocnvfv3  6047  eqfnov  6168  caoftrn  6308  suppimacnvfn  6459  suppssrst  6474  suppssrgst  6475  mpoxopovel  6485  rntpos  6501  ordgt0ge1  6681  iinerm  6854  erinxp  6856  qliftfun  6864  mapdm0  6910  elfi2  7272  fifo  7280  2omap  7282  inl11  7369  ctssdccl  7415  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  omniwomnimkv  7471  pr2nelem  7501  indpi  7673  genpdflem  7838  genpdisj  7854  genpassl  7855  genpassu  7856  ltnqpri  7925  ltpopr  7926  ltexprlemm  7931  ltexprlemdisj  7937  ltexprlemloc  7938  ltrennb  8185  letri3  8370  letr  8372  ltneg  8754  leneg  8757  reapltxor  8881  apsym  8898  suprnubex  9247  suprleubex  9248  elnnnn0  9559  fcdmnn0fsupp  9569  zrevaddcl  9648  znnsub  9649  znn0sub  9663  prime  9698  eluz2  9880  eluz2b1  9954  nn01to3  9970  qrevaddcl  9997  xrletri3  10159  xrletr  10163  iccid  10280  elicopnf  10324  fzsplit2  10407  fzsplit3  10410  fzsn  10424  fzpr  10436  uzsplit  10451  fvinim0ffz  10612  lt2sqi  11016  le2sqi  11017  sseqn  11231  ccatlcan  11438  ccatrcan  11439  abs00ap  11775  iooinsup  11990  mertenslem2  12250  fprod2dlemstep  12336  gcddiv  12743  algcvgblem  12774  isprm3  12843  dvdsfi  12964  ballotfilemodife  13187  imasmnd2  13710  imasgrp2  13866  issubg  13929  resgrpisgrp  13951  eqgval  13979  imasrng  14198  ring1  14305  imasring  14310  crngunit  14359  lssle0  14649  lssats2  14691  zndvds  14926  znleval  14930  znleval2  14931  eltg2b  15048  discld  15130  opnssneib  15150  restbasg  15162  ssidcn  15204  cnptoprest2  15234  lmss  15240  txrest  15270  txlm  15273  imasnopn  15293  bldisj  15395  xmeter  15430  bl2ioo  15544  limcdifap  15656  issubgr  16381  bj-sseq  16703  nnti  16905  pw1nct  16916