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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr4g  223  bibi2i  227  3bior1fd  1393  3biant1d  1396  equsalh  1778  eueq3dc  3000  sbcel12g  3162  sbceqg  3163  sbcnel12g  3164  reldisj  3576  r19.3rm  3616  eldifpr  3736  eldiftp  3755  rabxp  4812  elrng  4971  iss  5109  eliniseg  5157  fcnvres  5575  dffv3g  5691  funimass4  5753  fndmdif  5814  fneqeql  5817  funimass3  5825  elrnrexdmb  5848  dff4im  5854  fconst4m  5935  elunirn  5972  riota1  6058  riota2df  6060  f1ocnvfv3  6074  eqfnov  6195  caoftrn  6335  suppimacnvfn  6486  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  rntpos  6528  ordgt0ge1  6708  iinerm  6881  erinxp  6883  qliftfun  6891  mapdm0  6937  elfi2  7306  fifo  7314  2omap  7318  inl11  7405  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  omniwomnimkv  7507  pr2nelem  7537  indpi  7709  genpdflem  7874  genpdisj  7890  genpassl  7891  genpassu  7892  ltnqpri  7961  ltpopr  7962  ltexprlemm  7967  ltexprlemdisj  7973  ltexprlemloc  7974  ltrennb  8221  letri3  8406  letr  8408  ltneg  8790  leneg  8793  reapltxor  8918  apsym  8935  suprnubex  9284  suprleubex  9285  elnnnn0  9608  fcdmnn0fsupp  9618  zrevaddcl  9697  znnsub  9698  znn0sub  9712  prime  9747  eluz2  9929  eluz2b1  10003  nn01to3  10019  qrevaddcl  10046  xrletri3  10208  xrletr  10212  iccid  10329  elicopnf  10373  fzsplit2  10457  fzsplit3  10460  fzsn  10474  fzpr  10486  uzsplit  10501  fvinim0ffz  10662  lt2sqi  11066  le2sqi  11067  sseqn  11281  hashf1lem1  11287  ccatlcan  11492  ccatrcan  11493  abs00ap  11830  iooinsup  12045  mertenslem2  12305  fprod2dlemstep  12391  gcddiv  12798  algcvgblem  12829  isprm3  12898  dvdsfi  13019  ballotfilemodife  13242  imasmnd2  13761  imasgrp2  13915  issubg  13978  resgrpisgrp  14000  eqgval  14028  imasrng  14257  ring1  14366  imasring  14371  crngunit  14420  lssle0  14711  lssats2  14753  zndvds  14986  znleval  14990  znleval2  14991  eltg2b  15157  discld  15239  opnssneib  15259  restbasg  15271  ssidcn  15313  cnptoprest2  15343  lmss  15349  txrest  15379  txlm  15382  imasnopn  15402  bldisj  15504  xmeter  15539  bl2ioo  15653  limcdifap  15765  issubgr  16510  bj-sseq  16832  nnti  17034  pw1nct  17045