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  2926  sbcel12g  3087  sbceqg  3088  sbcnel12g  3089  reldisj  3489  r19.3rm  3526  eldifpr  3634  eldiftp  3653  rabxp  4681  elrng  4836  iss  4971  eliniseg  5016  fcnvres  5418  dffv3g  5530  funimass4  5587  fndmdif  5642  fneqeql  5645  funimass3  5653  elrnrexdmb  5677  dff4im  5683  fconst4m  5757  elunirn  5788  riota1  5871  riota2df  5873  f1ocnvfv3  5886  eqfnov  6004  caoftrn  6133  mpoxopovel  6267  rntpos  6283  ordgt0ge1  6461  iinerm  6634  erinxp  6636  qliftfun  6644  mapdm0  6690  elfi2  7002  fifo  7010  inl11  7095  ctssdccl  7141  isomnimap  7166  ismkvmap  7183  iswomnimap  7195  omniwomnimkv  7196  pr2nelem  7221  indpi  7372  genpdflem  7537  genpdisj  7553  genpassl  7554  genpassu  7555  ltnqpri  7624  ltpopr  7625  ltexprlemm  7630  ltexprlemdisj  7636  ltexprlemloc  7637  ltrennb  7884  letri3  8069  letr  8071  ltneg  8450  leneg  8453  reapltxor  8577  apsym  8594  suprnubex  8941  suprleubex  8942  elnnnn0  9250  zrevaddcl  9334  znnsub  9335  znn0sub  9349  prime  9383  eluz2  9565  eluz2b1  9633  nn01to3  9649  qrevaddcl  9676  xrletri3  9836  xrletr  9840  iccid  9957  elicopnf  10001  fzsplit2  10082  fzsn  10098  fzpr  10109  uzsplit  10124  fvinim0ffz  10273  lt2sqi  10642  le2sqi  10643  abs00ap  11106  iooinsup  11320  mertenslem2  11579  fprod2dlemstep  11665  gcddiv  12055  algcvgblem  12084  isprm3  12153  phisum  12275  imasgrp2  13067  issubg  13129  resgrpisgrp  13151  eqgval  13179  imasrng  13327  ring1  13428  imasring  13431  crngunit  13478  lssle0  13705  lssats2  13747  eltg2b  14031  discld  14113  opnssneib  14133  restbasg  14145  ssidcn  14187  cnptoprest2  14217  lmss  14223  txrest  14253  txlm  14256  imasnopn  14276  bldisj  14378  xmeter  14413  bl2ioo  14519  limcdifap  14608  bj-sseq  15022  nnti  15223  pw1nct  15231