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 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  con2bi  356  xorneg2  1544  sbrimvwOLD  2128  2eu4  2684  2eu5  2685  r19.41v  3195  r3ex  3204  r19.41  3269  sbralie  3343  sbralieOLD  3345  pm13.183  3628  euxfrw  3687  euxfr  3689  euind  3690  rmo4  3696  rmo3f  3700  2reu5lem3  3723  rmo3  3845  difin  4227  indifdi  4249  dftr5  5215  axsepgfromrep  5248  inuni  5310  reusv2lem4  5362  rabxp  5699  elvvv  5727  eliunxp  5813  elidinxp  6036  imadisj  6072  idrefALT  6103  intirr  6108  resco  6240  funcnv3  6595  fncnv  6598  fun11  6599  fununi  6600  mptfnf  6660  f1mpt  7249  mpomptx  7513  uniuni  7749  frxp  8110  xpord2pred  8129  xpord2indlem  8131  oeeu  8577  ixp0x  8912  xpcomco  9043  dffi3  9379  wemapsolem  9500  cardval3  9926  kmlem4  10125  kmlem12  10133  kmlem14  10135  kmlem15  10136  kmlem16  10137  fpwwe2  10616  axgroth4  10805  ltexprlem4  11012  bitsmod  16482  pythagtrip  16882  isstruct  17200  pgpfac1  20140  pgpfac  20144  basdif0  23067  ntreq0  23191  tgcmp  23515  tx1cn  23723  rnelfmlem  24066  phtpcer  25111  iscvsp  25244  caucfil  25399  minveclem1  25540  ovoliunlem1  25618  mdegleb  26178  eqcuts2  27933  dmcuts  27938  made0  28010  mulsuniflem  28296  istrkg2ld  28683  numedglnl  29399  usgr2pth0  30019  adjbd1o  32342  nmo  32742  dmrab  32749  difrab2  32750  mpomptxf  32931  ccfldextdgrr  33974  fldextrspunlsplem  33975  isros  34470  1stmbfm  34562  bnj976  35078  bnj1143  35090  bnj1533  35152  bnj864  35222  bnj983  35251  bnj1174  35303  bnj1175  35304  bnj1280  35320  axregs  35442  onvf1odlem2  35454  cvmlift2lem12  35672  axacprim  36065  dfrecs2  36308  andnand1  36769  mh-infprim1bi  36914  bj-snglc  37461  bj-disj2r  37520  bj-dfmpoa  37615  bj-mpomptALT  37616  mptsnunlem  37839  wl-df3xor2  37970  wl-df4-3mintru2  37988  wl-cases2-dnf  38022  wl-euae  38027  itg2addnc  38180  asindmre  38209  brres2  38779  brxrn2  38890  dfxrn2  38891  inxpxrn  38924  dfsuccl4  38980  refsymrel2  39157  refsymrel3  39158  dfeqvrel2  39180  dfeqvrel3  39181  isopos  39811  dihglblem6  41971  dihglb2  41973  fgraphopab  43787  unielss  43802  dflim5  43913  ifpid2g  44076  ifpim23g  44078  rp-fakeanorass  44096  en2pr  44130  elmapintrab  44159  relnonrel  44170  undmrnresiss  44187  elintima  44236  relexp0eq  44284  iunrelexp0  44285  dffrege115  44561  frege131  44577  frege133  44579  ntrneikb  44677  elnev  45006  onfrALTlem5  45110  onfrALTlem5VD  45452  ndisj2  45630  ndmaovcom  47798  usgrexmpl2nb3  48655  eliunxp2  48966  mpomptx2  48967  mo0sn  49446  i0oii  49550  io1ii  49551  alimp-no-surprise  50411  alsi-no-surprise  50426