Theorem 3bitr2i 299

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	⊢ (𝜑 ↔ 𝜓)
3bitr2i.2	⊢ (𝜒 ↔ 𝜓)
3bitr2i.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitr2i	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		3bitr2i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	1, 2	bitr4i 278	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 275	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  con2bi  353  xorneg2  1521  sbrimvw  2092  2eu4  2655  2eu5  2656  r19.41v  3175  r3ex  3184  r19.41  3250  sbralie  3336  sbralieOLD  3338  pm13.183  3650  euxfrw  3709  euxfr  3711  euind  3712  rmo4  3718  rmo3f  3722  2reu5lem3  3745  rmo3  3869  difin  4252  indifdi  4274  ab0orv  4363  dftr5  5238  axsepgfromrep  5269  inuni  5325  reusv2lem4  5376  rabxp  5707  elvvv  5735  eliunxp  5822  elidinxp  6036  imadisj  6072  idrefALT  6105  intirr  6112  resco  6244  funcnv3  6611  fncnv  6614  fun11  6615  fununi  6616  mptfnf  6678  f1mpt  7259  mpomptx  7525  uniuni  7761  frxp  8130  xpord2pred  8149  xpord2indlem  8151  oeeu  8620  ixp0x  8945  xpcomco  9081  1sdomOLD  9262  dffi3  9448  wemapsolem  9569  cardval3  9971  kmlem4  10173  kmlem12  10181  kmlem14  10183  kmlem15  10184  kmlem16  10185  fpwwe2  10662  axgroth4  10851  ltexprlem4  11058  bitsmod  16460  pythagtrip  16859  isstruct  17176  pgpfac1  20068  pgpfac  20072  basdif0  22896  ntreq0  23020  tgcmp  23344  tx1cn  23552  rnelfmlem  23895  phtpcer  24950  iscvsp  25084  caucfil  25240  minveclem1  25381  ovoliunlem1  25460  mdegleb  26026  eqscut2  27775  dmscut  27780  made0  27842  mulsuniflem  28109  istrkg2ld  28444  numedglnl  29128  usgr2pth0  29752  adjbd1o  32071  nmo  32476  dmrab  32483  difrab2  32484  mpomptxf  32660  ccfldextdgrr  33718  fldextrspunlsplem  33719  isros  34204  1stmbfm  34297  bnj976  34813  bnj1143  34826  bnj1533  34888  bnj864  34958  bnj983  34987  bnj1174  35039  bnj1175  35040  bnj1280  35056  cvmlift2lem12  35341  axacprim  35729  dfrecs2  35973  andnand1  36424  bj-snglc  36992  bj-disj2r  37051  bj-dfmpoa  37141  bj-mpomptALT  37142  mptsnunlem  37361  wl-df3xor2  37492  wl-df4-3mintru2  37510  wl-cases2-dnf  37535  wl-euae  37540  itg2addnc  37703  asindmre  37732  brres2  38291  brxrn2  38398  dfxrn2  38399  inxpxrn  38418  refsymrel2  38590  refsymrel3  38591  dfeqvrel2  38613  dfeqvrel3  38614  isopos  39203  dihglblem6  41364  dihglb2  41366  fgraphopab  43194  unielss  43209  dflim5  43320  ifpid2g  43484  ifpim23g  43486  rp-fakeanorass  43504  en2pr  43538  elmapintrab  43567  relnonrel  43578  undmrnresiss  43595  elintima  43644  relexp0eq  43692  iunrelexp0  43693  dffrege115  43969  frege131  43985  frege133  43987  ntrneikb  44085  elnev  44429  onfrALTlem5  44534  onfrALTlem5VD  44876  ndisj2  45042  ndmaovcom  47201  usgrexmpl2nb3  48005  eliunxp2  48276  mpomptx2  48277  mo0sn  48761  i0oii  48861  io1ii  48862  alimp-no-surprise  49612  alsi-no-surprise  49627