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  1389  3biant1d  1392  equsalh  1774  eueq3dc  2993  sbcel12g  3155  sbceqg  3156  sbcnel12g  3157  reldisj  3562  r19.3rm  3600  eldifpr  3718  eldiftp  3737  rabxp  4789  elrng  4948  iss  5086  eliniseg  5134  fcnvres  5552  dffv3g  5668  funimass4  5729  fndmdif  5785  fneqeql  5788  funimass3  5796  elrnrexdmb  5819  dff4im  5825  fconst4m  5906  elunirn  5941  riota1  6025  riota2df  6027  f1ocnvfv3  6041  eqfnov  6162  caoftrn  6301  suppimacnvfn  6448  suppssrst  6463  suppssrgst  6464  mpoxopovel  6474  rntpos  6490  ordgt0ge1  6670  iinerm  6843  erinxp  6845  qliftfun  6853  mapdm0  6899  elfi2  7261  fifo  7269  2omap  7271  inl11  7358  ctssdccl  7404  isomnimap  7430  ismkvmap  7447  iswomnimap  7459  omniwomnimkv  7460  pr2nelem  7490  indpi  7662  genpdflem  7827  genpdisj  7843  genpassl  7844  genpassu  7845  ltnqpri  7914  ltpopr  7915  ltexprlemm  7920  ltexprlemdisj  7926  ltexprlemloc  7927  ltrennb  8174  letri3  8359  letr  8361  ltneg  8741  leneg  8744  reapltxor  8868  apsym  8885  suprnubex  9232  suprleubex  9233  elnnnn0  9544  fcdmnn0fsupp  9554  zrevaddcl  9633  znnsub  9634  znn0sub  9648  prime  9683  eluz2  9865  eluz2b1  9939  nn01to3  9955  qrevaddcl  9982  xrletri3  10143  xrletr  10147  iccid  10264  elicopnf  10308  fzsplit2  10390  fzsn  10406  fzpr  10418  uzsplit  10433  fvinim0ffz  10594  lt2sqi  10996  le2sqi  10997  sseqn  11211  ccatlcan  11418  ccatrcan  11419  abs00ap  11755  iooinsup  11970  mertenslem2  12230  fprod2dlemstep  12316  gcddiv  12723  algcvgblem  12754  isprm3  12823  dvdsfi  12944  ballotfilemodife  13162  imasmnd2  13686  imasgrp2  13848  issubg  13911  resgrpisgrp  13933  eqgval  13961  imasrng  14121  ring1  14224  imasring  14229  crngunit  14278  lssle0  14569  lssats2  14611  zndvds  14846  znleval  14850  znleval2  14851  eltg2b  14968  discld  15050  opnssneib  15070  restbasg  15082  ssidcn  15124  cnptoprest2  15154  lmss  15160  txrest  15190  txlm  15193  imasnopn  15213  bldisj  15315  xmeter  15350  bl2ioo  15464  limcdifap  15576  issubgr  16301  bj-sseq  16613  nnti  16815  pw1nct  16826