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  1518  sbrimvw  2089  2eu4  2653  2eu5  2654  r19.41v  3187  r3ex  3196  r19.41  3261  sbralie  3356  pm13.183  3666  euxfrw  3730  euxfr  3732  euind  3733  rmo4  3739  rmo3f  3743  2reu5lem3  3766  rmo3  3898  difin  4278  indifdi  4300  ab0orv  4389  dftr5  5269  axsepgfromrep  5300  inuni  5356  reusv2lem4  5407  rabxp  5737  elvvv  5764  eliunxp  5851  elidinxp  6064  imadisj  6100  idrefALT  6134  intirr  6141  resco  6272  funcnv3  6638  fncnv  6641  fun11  6642  fununi  6643  mptfnf  6704  f1mpt  7281  mpomptx  7546  uniuni  7781  frxp  8150  xpord2pred  8169  xpord2indlem  8171  oeeu  8640  ixp0x  8965  xpcomco  9101  1sdomOLD  9283  dffi3  9469  wemapsolem  9588  cardval3  9990  kmlem4  10192  kmlem12  10200  kmlem14  10202  kmlem15  10203  kmlem16  10204  fpwwe2  10681  axgroth4  10870  ltexprlem4  11077  bitsmod  16470  pythagtrip  16868  isstruct  17186  pgpfac1  20115  pgpfac  20119  basdif0  22976  ntreq0  23101  tgcmp  23425  tx1cn  23633  rnelfmlem  23976  phtpcer  25041  iscvsp  25175  caucfil  25331  minveclem1  25472  ovoliunlem1  25551  mdegleb  26118  eqscut2  27866  dmscut  27871  made0  27927  mulsuniflem  28190  istrkg2ld  28483  numedglnl  29176  usgr2pth0  29798  adjbd1o  32114  nmo  32518  dmrab  32525  difrab2  32526  mpomptxf  32694  ccfldextdgrr  33697  isros  34149  1stmbfm  34242  bnj976  34770  bnj1143  34783  bnj1533  34845  bnj864  34915  bnj983  34944  bnj1174  34996  bnj1175  34997  bnj1280  35013  cvmlift2lem12  35299  axacprim  35687  dfrecs2  35932  andnand1  36384  bj-snglc  36952  bj-disj2r  37011  bj-dfmpoa  37101  bj-mpomptALT  37102  mptsnunlem  37321  wl-df3xor2  37452  wl-df4-3mintru2  37470  wl-cases2-dnf  37493  wl-euae  37498  itg2addnc  37661  asindmre  37690  brres2  38250  brxrn2  38357  dfxrn2  38358  inxpxrn  38377  refsymrel2  38549  refsymrel3  38550  dfeqvrel2  38572  dfeqvrel3  38573  isopos  39162  dihglblem6  41323  dihglb2  41325  fgraphopab  43192  unielss  43207  dflim5  43319  ifpid2g  43483  ifpim23g  43485  rp-fakeanorass  43503  en2pr  43537  elmapintrab  43566  relnonrel  43577  undmrnresiss  43594  elintima  43643  relexp0eq  43691  iunrelexp0  43692  dffrege115  43968  frege131  43984  frege133  43986  ntrneikb  44084  elnev  44434  onfrALTlem5  44540  onfrALTlem5VD  44883  ndisj2  44991  ndmaovcom  47155  usgrexmpl2nb3  47929  eliunxp2  48179  mpomptx2  48180  mo0sn  48664  i0oii  48716  io1ii  48717  alimp-no-surprise  49012  alsi-no-surprise  49027