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  2977  sbcel12g  3139  sbceqg  3140  sbcnel12g  3141  reldisj  3543  r19.3rm  3580  eldifpr  3693  eldiftp  3712  rabxp  4756  elrng  4913  iss  5051  eliniseg  5098  fcnvres  5511  dffv3g  5625  funimass4  5686  fndmdif  5742  fneqeql  5745  funimass3  5753  elrnrexdmb  5777  dff4im  5783  fconst4m  5863  elunirn  5896  riota1  5980  riota2df  5982  f1ocnvfv3  5996  eqfnov  6117  caoftrn  6257  mpoxopovel  6393  rntpos  6409  ordgt0ge1  6589  iinerm  6762  erinxp  6764  qliftfun  6772  mapdm0  6818  elfi2  7147  fifo  7155  inl11  7240  ctssdccl  7286  isomnimap  7312  ismkvmap  7329  iswomnimap  7341  omniwomnimkv  7342  pr2nelem  7372  indpi  7537  genpdflem  7702  genpdisj  7718  genpassl  7719  genpassu  7720  ltnqpri  7789  ltpopr  7790  ltexprlemm  7795  ltexprlemdisj  7801  ltexprlemloc  7802  ltrennb  8049  letri3  8235  letr  8237  ltneg  8617  leneg  8620  reapltxor  8744  apsym  8761  suprnubex  9108  suprleubex  9109  elnnnn0  9420  zrevaddcl  9505  znnsub  9506  znn0sub  9520  prime  9554  eluz2  9736  eluz2b1  9804  nn01to3  9820  qrevaddcl  9847  xrletri3  10008  xrletr  10012  iccid  10129  elicopnf  10173  fzsplit2  10254  fzsn  10270  fzpr  10281  uzsplit  10296  fvinim0ffz  10455  lt2sqi  10857  le2sqi  10858  ccatlcan  11258  ccatrcan  11259  abs00ap  11581  iooinsup  11796  mertenslem2  12055  fprod2dlemstep  12141  gcddiv  12548  algcvgblem  12579  isprm3  12648  dvdsfi  12769  imasmnd2  13493  imasgrp2  13655  issubg  13718  resgrpisgrp  13740  eqgval  13768  imasrng  13927  ring1  14030  imasring  14035  crngunit  14083  lssle0  14344  lssats2  14386  zndvds  14621  znleval  14625  znleval2  14626  eltg2b  14736  discld  14818  opnssneib  14838  restbasg  14850  ssidcn  14892  cnptoprest2  14922  lmss  14928  txrest  14958  txlm  14961  imasnopn  14981  bldisj  15083  xmeter  15118  bl2ioo  15232  limcdifap  15344  bj-sseq  16180  nnti  16385  2omap  16388  pw1nct  16398