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  2131  2eu4  2682  2eu5  2683  r19.41v  3196  r3ex  3205  r19.41  3270  sbralie  3342  sbralieOLD  3344  pm13.183  3623  euxfrw  3682  euxfr  3684  euind  3685  rmo4  3691  rmo3f  3695  2reu5lem3  3718  rmo3  3840  difin  4220  indifdi  4242  dftr5  5220  axsepgfromrep  5251  inuni  5316  reusv2lem4  5368  rabxp  5704  elvvv  5733  eliunxp  5821  elidinxp  6049  imadisj  6090  idrefALT  6120  intirr  6125  resco  6265  funcnv3  6635  fncnv  6638  fun11  6639  fununi  6640  mptfnf  6699  f1mpt  7291  mpomptx  7559  mpt3mpt  7712  uniuni  7803  frxp  8168  xpord2pred  8192  xpord2indlem  8194  oeeu  8643  ixp0x  8985  xpcomco  9117  dffi3  9453  wemapsolem  9574  karden  9989  cardval3  10063  kmlem4  10262  kmlem12  10270  kmlem14  10272  kmlem15  10273  kmlem16  10274  fpwwe2  10758  axgroth4  10947  ltexprlem4  11154  bitsmod  16638  pythagtrip  17044  isstruct  17362  pgpfac1  20329  pgpfac  20333  basdif0  23304  ntreq0  23428  tgcmp  23752  tx1cn  23961  rnelfmlem  24304  phtpcer  25349  iscvsp  25482  caucfil  25637  minveclem1  25778  ovoliunlem1  25856  mdegleb  26415  eqcuts2  28205  dmcuts  28210  made0  28282  mulsuniflem  28568  istrkg2ld  28955  numedglnl  29755  usgr2pth0  30384  adjbd1o  32720  nmo  33161  dmrab  33168  difrab2  33169  mpomptxf  33346  ccfldextdgrr  34387  fldextrspunlsplem  34388  isros  34884  1stmbfm  34975  bnj976  35491  bnj1143  35503  bnj1533  35565  bnj864  35635  bnj983  35664  bnj1174  35716  bnj1175  35717  bnj1280  35733  axregs  35920  onvf1odlem2  36045  cvmlift2lem12  36259  mirimanofffr  36642  axacprim  36663  dfrecs2  36905  andnand1  37380  mh-infprim1bi  37525  bj-snglc  38073  bj-disj2r  38132  bj-dfmpoa  38244  bj-mpomptALT  38245  mptsnunlem  38466  wl-df3xor2  38597  wl-df4-3mintru2  38615  wl-cases2-dnf  38649  wl-euae  38654  itg2addnc  38797  asindmre  38826  brres2  39408  brxrn2  39519  dfxrn2  39520  inxpxrn  39553  dfsuccl4  39609  refsymrel2  39786  refsymrel3  39787  dfeqvrel2  39809  dfeqvrel3  39810  isopos  40440  dihglblem6  42600  dihglb2  42602  fgraphopab  44408  unielss  44423  dflim5  44534  ifpid2g  44697  ifpim23g  44699  rp-fakeanorass  44717  en2pr  44751  elmapintrab  44780  relnonrel  44790  undmrnresiss  44807  elintima  44856  relexp0eq  44904  iunrelexp0  44905  dffrege115  45181  frege131  45197  frege133  45199  ntrneikb  45297  elnev  45623  onfrALTlem5  45727  onfrALTlem5VD  46069  ndisj2  46284  ndmaovcom  48490  usgrexmpl2nb3  49347  eliunxp2  49661  mpomptx2  49662  mo0sn  50142  i0oii  50249  io1ii  50250  alimp-no-surprise  51189  als-no-surprise  51214