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  4814  elrng  4973  iss  5112  eliniseg  5160  fcnvres  5578  dffv3g  5694  funimass4  5756  fndmdif  5817  fneqeql  5820  funimass3  5828  elrnrexdmb  5851  dff4im  5857  fconst4m  5938  elunirn  5975  riota1  6061  riota2df  6063  f1ocnvfv3  6077  eqfnov  6198  caoftrn  6339  suppimacnvfn  6490  suppssrst  6505  suppssrgst  6506  mpoxopovel  6516  rntpos  6532  ordgt0ge1  6712  iinerm  6885  erinxp  6887  qliftfun  6895  mapdm0  6941  relresfin  7269  elfi2  7312  fifo  7320  2omap  7325  inl11  7412  ctssdccl  7458  isomnimap  7484  ismkvmap  7501  iswomnimap  7513  omniwomnimkv  7514  pr2nelem  7544  indpi  7716  genpdflem  7881  genpdisj  7897  genpassl  7898  genpassu  7899  ltnqpri  7968  ltpopr  7969  ltexprlemm  7974  ltexprlemdisj  7980  ltexprlemloc  7981  ltrennb  8228  letri3  8413  letr  8415  ltneg  8798  leneg  8801  reapltxor  8926  apsym  8943  suprnubex  9292  suprleubex  9293  elnnnn0  9618  fcdmnn0fsupp  9628  zrevaddcl  9707  znnsub  9708  znn0sub  9722  prime  9757  eluz2  9944  eluz2b1  10018  nn01to3  10034  qrevaddcl  10061  xrletri3  10224  xrletr  10228  iccid  10345  elicopnf  10389  fzsplit2  10473  fzsplit3  10476  fzsn  10490  fzpr  10502  uzsplit  10517  fvinim0ffz  10678  lt2sqi  11086  le2sqi  11087  sseqn  11302  hashf1lem1  11308  ccatlcan  11513  ccatrcan  11514  abs00ap  11851  iooinsup  12069  mertenslem2  12329  fprod2dlemstep  12415  gcddiv  12822  algcvgblem  12853  isprm3  12922  dvdsfi  13047  ballotfilemodife  13299  imasmnd2  13819  imasgrp2  13973  issubg  14036  resgrpisgrp  14058  eqgval  14086  gsumcom2fi  14276  imasrng  14363  ring1  14472  imasring  14479  crngunit  14528  lssle0  14819  lssats2  14861  zndvds  15094  znleval  15098  znleval2  15099  eltg2b  15292  discld  15374  opnssneib  15394  restbasg  15406  ssidcn  15448  cnptoprest2  15478  lmss  15484  txrest  15514  txlm  15517  imasnopn  15537  bldisj  15639  xmeter  15674  bl2ioo  15788  limcdifap  15900  bposlem6  16328  issubgr  16715  bj-sseq  17037  nnti  17239  pw1nct  17250