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  2990  sbcel12g  3152  sbceqg  3153  sbcnel12g  3154  reldisj  3559  r19.3rm  3597  eldifpr  3715  eldiftp  3734  rabxp  4786  elrng  4945  iss  5083  eliniseg  5131  fcnvres  5549  dffv3g  5665  funimass4  5726  fndmdif  5782  fneqeql  5785  funimass3  5793  elrnrexdmb  5816  dff4im  5822  fconst4m  5903  elunirn  5938  riota1  6022  riota2df  6024  f1ocnvfv3  6038  eqfnov  6159  caoftrn  6298  suppimacnvfn  6445  suppssrst  6460  suppssrgst  6461  mpoxopovel  6471  rntpos  6487  ordgt0ge1  6667  iinerm  6840  erinxp  6842  qliftfun  6850  mapdm0  6896  elfi2  7258  fifo  7266  2omap  7268  inl11  7355  ctssdccl  7401  isomnimap  7427  ismkvmap  7444  iswomnimap  7456  omniwomnimkv  7457  pr2nelem  7487  indpi  7653  genpdflem  7818  genpdisj  7834  genpassl  7835  genpassu  7836  ltnqpri  7905  ltpopr  7906  ltexprlemm  7911  ltexprlemdisj  7917  ltexprlemloc  7918  ltrennb  8165  letri3  8350  letr  8352  ltneg  8732  leneg  8735  reapltxor  8859  apsym  8876  suprnubex  9223  suprleubex  9224  elnnnn0  9535  fcdmnn0fsupp  9545  zrevaddcl  9624  znnsub  9625  znn0sub  9639  prime  9673  eluz2  9855  eluz2b1  9929  nn01to3  9945  qrevaddcl  9972  xrletri3  10133  xrletr  10137  iccid  10254  elicopnf  10298  fzsplit2  10380  fzsn  10396  fzpr  10407  uzsplit  10422  fvinim0ffz  10583  lt2sqi  10985  le2sqi  10986  sseqn  11196  ccatlcan  11403  ccatrcan  11404  abs00ap  11740  iooinsup  11955  mertenslem2  12215  fprod2dlemstep  12301  gcddiv  12708  algcvgblem  12739  isprm3  12808  dvdsfi  12929  imasmnd2  13654  imasgrp2  13816  issubg  13879  resgrpisgrp  13901  eqgval  13929  imasrng  14089  ring1  14192  imasring  14197  crngunit  14245  lssle0  14507  lssats2  14549  zndvds  14784  znleval  14788  znleval2  14789  eltg2b  14906  discld  14988  opnssneib  15008  restbasg  15020  ssidcn  15062  cnptoprest2  15092  lmss  15098  txrest  15128  txlm  15131  imasnopn  15151  bldisj  15253  xmeter  15288  bl2ioo  15402  limcdifap  15514  issubgr  16239  bj-sseq  16551  nnti  16753  pw1nct  16764