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  1520  sbrimvw  2090  2eu4  2653  2eu5  2654  r19.41v  3176  r3ex  3185  r19.41  3249  sbralie  3341  pm13.183  3649  euxfrw  3709  euxfr  3711  euind  3712  rmo4  3718  rmo3f  3722  2reu5lem3  3745  rmo3  3869  difin  4252  indifdi  4274  ab0orv  4363  dftr5  5243  axsepgfromrep  5274  inuni  5330  reusv2lem4  5381  rabxp  5713  elvvv  5741  eliunxp  5828  elidinxp  6042  imadisj  6078  idrefALT  6111  intirr  6118  resco  6250  funcnv3  6616  fncnv  6619  fun11  6620  fununi  6621  mptfnf  6683  f1mpt  7263  mpomptx  7528  uniuni  7764  frxp  8133  xpord2pred  8152  xpord2indlem  8154  oeeu  8623  ixp0x  8948  xpcomco  9084  1sdomOLD  9267  dffi3  9453  wemapsolem  9572  cardval3  9974  kmlem4  10176  kmlem12  10184  kmlem14  10186  kmlem15  10187  kmlem16  10188  fpwwe2  10665  axgroth4  10854  ltexprlem4  11061  bitsmod  16456  pythagtrip  16855  isstruct  17172  pgpfac1  20069  pgpfac  20073  basdif0  22908  ntreq0  23032  tgcmp  23356  tx1cn  23564  rnelfmlem  23907  phtpcer  24964  iscvsp  25098  caucfil  25254  minveclem1  25395  ovoliunlem1  25474  mdegleb  26040  eqscut2  27788  dmscut  27793  made0  27849  mulsuniflem  28112  istrkg2ld  28405  numedglnl  29090  usgr2pth0  29714  adjbd1o  32033  nmo  32438  dmrab  32445  difrab2  32446  mpomptxf  32623  ccfldextdgrr  33664  fldextrspunlsplem  33665  isros  34144  1stmbfm  34237  bnj976  34766  bnj1143  34779  bnj1533  34841  bnj864  34911  bnj983  34940  bnj1174  34992  bnj1175  34993  bnj1280  35009  cvmlift2lem12  35294  axacprim  35682  dfrecs2  35926  andnand1  36377  bj-snglc  36945  bj-disj2r  37004  bj-dfmpoa  37094  bj-mpomptALT  37095  mptsnunlem  37314  wl-df3xor2  37445  wl-df4-3mintru2  37463  wl-cases2-dnf  37488  wl-euae  37493  itg2addnc  37656  asindmre  37685  brres2  38244  brxrn2  38351  dfxrn2  38352  inxpxrn  38371  refsymrel2  38543  refsymrel3  38544  dfeqvrel2  38566  dfeqvrel3  38567  isopos  39156  dihglblem6  41317  dihglb2  41319  fgraphopab  43193  unielss  43208  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  44429  onfrALTlem5  44534  onfrALTlem5VD  44877  ndisj2  45028  ndmaovcom  47190  usgrexmpl2nb3  47966  eliunxp2  48223  mpomptx2  48224  mo0sn  48708  i0oii  48801  io1ii  48802  alimp-no-surprise  49395  alsi-no-surprise  49410