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  1388  3biant1d  1391  equsalh  1774  eueq3dc  2980  sbcel12g  3142  sbceqg  3143  sbcnel12g  3144  reldisj  3546  r19.3rm  3583  eldifpr  3696  eldiftp  3715  rabxp  4763  elrng  4921  iss  5059  eliniseg  5106  fcnvres  5520  dffv3g  5635  funimass4  5696  fndmdif  5752  fneqeql  5755  funimass3  5763  elrnrexdmb  5787  dff4im  5793  fconst4m  5874  elunirn  5907  riota1  5991  riota2df  5993  f1ocnvfv3  6007  eqfnov  6128  caoftrn  6268  mpoxopovel  6407  rntpos  6423  ordgt0ge1  6603  iinerm  6776  erinxp  6778  qliftfun  6786  mapdm0  6832  elfi2  7171  fifo  7179  inl11  7264  ctssdccl  7310  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  omniwomnimkv  7366  pr2nelem  7396  indpi  7562  genpdflem  7727  genpdisj  7743  genpassl  7744  genpassu  7745  ltnqpri  7814  ltpopr  7815  ltexprlemm  7820  ltexprlemdisj  7826  ltexprlemloc  7827  ltrennb  8074  letri3  8260  letr  8262  ltneg  8642  leneg  8645  reapltxor  8769  apsym  8786  suprnubex  9133  suprleubex  9134  elnnnn0  9445  zrevaddcl  9530  znnsub  9531  znn0sub  9545  prime  9579  eluz2  9761  eluz2b1  9835  nn01to3  9851  qrevaddcl  9878  xrletri3  10039  xrletr  10043  iccid  10160  elicopnf  10204  fzsplit2  10285  fzsn  10301  fzpr  10312  uzsplit  10327  fvinim0ffz  10488  lt2sqi  10890  le2sqi  10891  ccatlcan  11300  ccatrcan  11301  abs00ap  11624  iooinsup  11839  mertenslem2  12099  fprod2dlemstep  12185  gcddiv  12592  algcvgblem  12623  isprm3  12692  dvdsfi  12813  imasmnd2  13537  imasgrp2  13699  issubg  13762  resgrpisgrp  13784  eqgval  13812  imasrng  13972  ring1  14075  imasring  14080  crngunit  14128  lssle0  14389  lssats2  14431  zndvds  14666  znleval  14670  znleval2  14671  eltg2b  14781  discld  14863  opnssneib  14883  restbasg  14895  ssidcn  14937  cnptoprest2  14967  lmss  14973  txrest  15003  txlm  15006  imasnopn  15026  bldisj  15128  xmeter  15163  bl2ioo  15277  limcdifap  15389  issubgr  16111  bj-sseq  16409  nnti  16612  2omap  16615  pw1nct  16625