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  1737  eueq3dc  2934  sbcel12g  3095  sbceqg  3096  sbcnel12g  3097  reldisj  3498  r19.3rm  3535  eldifpr  3645  eldiftp  3664  rabxp  4696  elrng  4853  iss  4988  eliniseg  5035  fcnvres  5437  dffv3g  5550  funimass4  5607  fndmdif  5663  fneqeql  5666  funimass3  5674  elrnrexdmb  5698  dff4im  5704  fconst4m  5778  elunirn  5809  riota1  5892  riota2df  5894  f1ocnvfv3  5907  eqfnov  6025  caoftrn  6158  mpoxopovel  6294  rntpos  6310  ordgt0ge1  6488  iinerm  6661  erinxp  6663  qliftfun  6671  mapdm0  6717  elfi2  7031  fifo  7039  inl11  7124  ctssdccl  7170  isomnimap  7196  ismkvmap  7213  iswomnimap  7225  omniwomnimkv  7226  pr2nelem  7251  indpi  7402  genpdflem  7567  genpdisj  7583  genpassl  7584  genpassu  7585  ltnqpri  7654  ltpopr  7655  ltexprlemm  7660  ltexprlemdisj  7666  ltexprlemloc  7667  ltrennb  7914  letri3  8100  letr  8102  ltneg  8481  leneg  8484  reapltxor  8608  apsym  8625  suprnubex  8972  suprleubex  8973  elnnnn0  9283  zrevaddcl  9367  znnsub  9368  znn0sub  9382  prime  9416  eluz2  9598  eluz2b1  9666  nn01to3  9682  qrevaddcl  9709  xrletri3  9870  xrletr  9874  iccid  9991  elicopnf  10035  fzsplit2  10116  fzsn  10132  fzpr  10143  uzsplit  10158  fvinim0ffz  10308  lt2sqi  10698  le2sqi  10699  abs00ap  11206  iooinsup  11420  mertenslem2  11679  fprod2dlemstep  11765  gcddiv  12156  algcvgblem  12187  isprm3  12256  phisum  12378  imasgrp2  13180  issubg  13243  resgrpisgrp  13265  eqgval  13293  imasrng  13452  ring1  13555  imasring  13560  crngunit  13607  lssle0  13868  lssats2  13910  zndvds  14137  znleval  14141  znleval2  14142  eltg2b  14222  discld  14304  opnssneib  14324  restbasg  14336  ssidcn  14378  cnptoprest2  14408  lmss  14414  txrest  14444  txlm  14447  imasnopn  14467  bldisj  14569  xmeter  14604  bl2ioo  14710  limcdifap  14816  bj-sseq  15284  nnti  15485  pw1nct  15493