Theorem 3bitr2i 302

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 281	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 278	1 ⊢ (𝜑 ↔ 𝜃)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con2bi  356  xorneg2  1550  sbrimvwOLD  2128  2eu4  2679  2eu5  2680  r19.41v  3192  r3ex  3201  r19.41  3266  sbralie  3338  sbralieOLD  3340  pm13.183  3619  euxfrw  3678  euxfr  3680  euind  3681  rmo4  3687  rmo3f  3691  2reu5lem3  3714  rmo3  3835  difin  4217  indifdi  4239  dftr5  5215  axsepgfromrep  5246  inuni  5310  reusv2lem4  5362  rabxp  5698  elvvv  5726  eliunxp  5813  elidinxp  6035  imadisj  6076  idrefALT  6106  intirr  6111  resco  6251  funcnv3  6611  fncnv  6614  fun11  6615  fununi  6616  mptfnf  6675  f1mpt  7266  mpomptx  7534  mpt3mpt  7686  uniuni  7777  frxp  8141  xpord2pred  8165  xpord2indlem  8167  oeeu  8616  ixp0x  8958  xpcomco  9090  dffi3  9427  wemapsolem  9548  karden  9963  cardval3  10037  kmlem4  10236  kmlem12  10244  kmlem14  10246  kmlem15  10247  kmlem16  10248  fpwwe2  10732  axgroth4  10921  ltexprlem4  11128  bitsmod  16612  pythagtrip  17018  isstruct  17336  pgpfac1  20302  pgpfac  20306  basdif0  23277  ntreq0  23401  tgcmp  23725  tx1cn  23934  rnelfmlem  24277  phtpcer  25322  iscvsp  25455  caucfil  25610  minveclem1  25751  ovoliunlem1  25829  mdegleb  26388  eqcuts2  28178  dmcuts  28183  made0  28255  mulsuniflem  28541  istrkg2ld  28928  numedglnl  29728  usgr2pth0  30357  adjbd1o  32693  nmo  33134  dmrab  33141  difrab2  33142  mpomptxf  33320  ccfldextdgrr  34351  fldextrspunlsplem  34352  isros  34848  1stmbfm  34939  bnj976  35455  bnj1143  35467  bnj1533  35529  bnj864  35599  bnj983  35628  bnj1174  35680  bnj1175  35681  bnj1280  35697  axregs  35864  onvf1odlem2  35952  cvmlift2lem12  36166  axacprim  36565  dfrecs2  36807  andnand1  37282  mh-infprim1bi  37427  bj-snglc  37975  bj-disj2r  38034  bj-dfmpoa  38133  bj-mpomptALT  38134  mptsnunlem  38355  wl-df3xor2  38486  wl-df4-3mintru2  38504  wl-cases2-dnf  38538  wl-euae  38543  itg2addnc  38686  asindmre  38715  brres2  39299  brxrn2  39410  dfxrn2  39411  inxpxrn  39444  dfsuccl4  39500  refsymrel2  39677  refsymrel3  39678  dfeqvrel2  39700  dfeqvrel3  39701  isopos  40331  dihglblem6  42491  dihglb2  42493  fgraphopab  44299  unielss  44314  dflim5  44425  ifpid2g  44588  ifpim23g  44590  rp-fakeanorass  44608  en2pr  44642  elmapintrab  44671  relnonrel  44681  undmrnresiss  44698  elintima  44747  relexp0eq  44795  iunrelexp0  44796  dffrege115  45072  frege131  45088  frege133  45090  ntrneikb  45188  elnev  45515  onfrALTlem5  45619  onfrALTlem5VD  45961  ndisj2  46162  ndmaovcom  48369  usgrexmpl2nb3  49226  eliunxp2  49540  mpomptx2  49541  mo0sn  50021  i0oii  50128  io1ii  50129  alimp-no-surprise  51046  als-no-surprise  51071