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  equsalh  1740  eueq3dc  2938  sbcel12g  3099  sbceqg  3100  sbcnel12g  3101  reldisj  3503  r19.3rm  3540  eldifpr  3650  eldiftp  3669  rabxp  4701  elrng  4858  iss  4993  eliniseg  5040  fcnvres  5444  dffv3g  5557  funimass4  5614  fndmdif  5670  fneqeql  5673  funimass3  5681  elrnrexdmb  5705  dff4im  5711  fconst4m  5785  elunirn  5816  riota1  5899  riota2df  5901  f1ocnvfv3  5914  eqfnov  6033  caoftrn  6172  mpoxopovel  6308  rntpos  6324  ordgt0ge1  6502  iinerm  6675  erinxp  6677  qliftfun  6685  mapdm0  6731  elfi2  7047  fifo  7055  inl11  7140  ctssdccl  7186  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  omniwomnimkv  7242  pr2nelem  7272  indpi  7428  genpdflem  7593  genpdisj  7609  genpassl  7610  genpassu  7611  ltnqpri  7680  ltpopr  7681  ltexprlemm  7686  ltexprlemdisj  7692  ltexprlemloc  7693  ltrennb  7940  letri3  8126  letr  8128  ltneg  8508  leneg  8511  reapltxor  8635  apsym  8652  suprnubex  8999  suprleubex  9000  elnnnn0  9311  zrevaddcl  9395  znnsub  9396  znn0sub  9410  prime  9444  eluz2  9626  eluz2b1  9694  nn01to3  9710  qrevaddcl  9737  xrletri3  9898  xrletr  9902  iccid  10019  elicopnf  10063  fzsplit2  10144  fzsn  10160  fzpr  10171  uzsplit  10186  fvinim0ffz  10336  lt2sqi  10738  le2sqi  10739  abs00ap  11246  iooinsup  11461  mertenslem2  11720  fprod2dlemstep  11806  gcddiv  12213  algcvgblem  12244  isprm3  12313  dvdsfi  12434  imasmnd2  13156  imasgrp2  13318  issubg  13381  resgrpisgrp  13403  eqgval  13431  imasrng  13590  ring1  13693  imasring  13698  crngunit  13745  lssle0  14006  lssats2  14048  zndvds  14283  znleval  14287  znleval2  14288  eltg2b  14376  discld  14458  opnssneib  14478  restbasg  14490  ssidcn  14532  cnptoprest2  14562  lmss  14568  txrest  14598  txlm  14601  imasnopn  14621  bldisj  14723  xmeter  14758  bl2ioo  14872  limcdifap  14984  bj-sseq  15524  nnti  15725  2omap  15728  pw1nct  15736