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  1551  sbrimvwOLD  2129  2eu4  2679  2eu5  2680  r19.41v  3192  r3ex  3201  r19.41  3266  sbralie  3338  sbralieOLD  3340  pm13.183  3620  euxfrw  3679  euxfr  3681  euind  3682  rmo4  3688  rmo3f  3692  2reu5lem3  3715  rmo3  3836  difin  4218  indifdi  4240  dftr5  5216  axsepgfromrep  5249  inuni  5314  reusv2lem4  5366  rabxp  5703  elvvv  5731  eliunxp  5817  elidinxp  6040  imadisj  6076  idrefALT  6107  intirr  6112  resco  6246  funcnv3  6603  fncnv  6606  fun11  6607  fununi  6608  mptfnf  6667  f1mpt  7258  mpomptx  7526  uniuni  7761  frxp  8124  xpord2pred  8143  xpord2indlem  8145  oeeu  8591  ixp0x  8933  xpcomco  9065  dffi3  9401  wemapsolem  9522  karden  9898  cardval3  9957  kmlem4  10156  kmlem12  10164  kmlem14  10166  kmlem15  10167  kmlem16  10168  fpwwe2  10652  axgroth4  10841  ltexprlem4  11048  bitsmod  16526  pythagtrip  16926  isstruct  17244  pgpfac1  20209  pgpfac  20213  basdif0  23178  ntreq0  23302  tgcmp  23626  tx1cn  23835  rnelfmlem  24178  phtpcer  25223  iscvsp  25356  caucfil  25511  minveclem1  25652  ovoliunlem1  25730  mdegleb  26289  eqcuts2  28051  dmcuts  28056  made0  28128  mulsuniflem  28414  istrkg2ld  28801  numedglnl  29601  usgr2pth0  30230  adjbd1o  32566  nmo  32965  dmrab  32972  difrab2  32973  mpomptxf  33151  ccfldextdgrr  34182  fldextrspunlsplem  34183  isros  34679  1stmbfm  34771  bnj976  35287  bnj1143  35299  bnj1533  35361  bnj864  35431  bnj983  35460  bnj1174  35512  bnj1175  35513  bnj1280  35529  axregs  35665  onvf1odlem2  35701  cvmlift2lem12  35893  axacprim  36286  dfrecs2  36529  andnand1  37020  mh-infprim1bi  37165  bj-snglc  37713  bj-disj2r  37772  bj-dfmpoa  37868  bj-mpomptALT  37869  mptsnunlem  38092  wl-df3xor2  38223  wl-df4-3mintru2  38241  wl-cases2-dnf  38275  wl-euae  38280  itg2addnc  38423  asindmre  38452  brres2  39021  brxrn2  39132  dfxrn2  39133  inxpxrn  39166  dfsuccl4  39222  refsymrel2  39399  refsymrel3  39400  dfeqvrel2  39422  dfeqvrel3  39423  isopos  40053  dihglblem6  42213  dihglb2  42215  fgraphopab  44044  unielss  44059  dflim5  44170  ifpid2g  44333  ifpim23g  44335  rp-fakeanorass  44353  en2pr  44387  elmapintrab  44416  relnonrel  44427  undmrnresiss  44444  elintima  44493  relexp0eq  44541  iunrelexp0  44542  dffrege115  44818  frege131  44834  frege133  44836  ntrneikb  44934  elnev  45261  onfrALTlem5  45365  onfrALTlem5VD  45707  ndisj2  45885  ndmaovcom  48093  usgrexmpl2nb3  48950  eliunxp2  49264  mpomptx2  49265  mo0sn  49744  i0oii  49846  io1ii  49847  alimp-no-surprise  50710  als-no-surprise  50735