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  1523  sbrimvw  2097  2eu4  2656  2eu5  2657  r19.41v  3168  r3ex  3177  r19.41  3242  sbralie  3316  sbralieOLD  3318  pm13.183  3609  euxfrw  3668  euxfr  3670  euind  3671  rmo4  3677  rmo3f  3681  2reu5lem3  3704  rmo3  3828  difin  4213  indifdi  4235  dftr5  5197  axsepgfromrep  5229  inuni  5285  reusv2lem4  5336  rabxp  5670  elvvv  5698  eliunxp  5784  elidinxp  6001  imadisj  6037  idrefALT  6068  intirr  6073  resco  6206  funcnv3  6560  fncnv  6563  fun11  6564  fununi  6565  mptfnf  6625  f1mpt  7207  mpomptx  7471  uniuni  7707  frxp  8067  xpord2pred  8086  xpord2indlem  8088  oeeu  8530  ixp0x  8865  xpcomco  8996  dffi3  9335  wemapsolem  9456  cardval3  9865  kmlem4  10065  kmlem12  10073  kmlem14  10075  kmlem15  10076  kmlem16  10077  fpwwe2  10555  axgroth4  10744  ltexprlem4  10951  bitsmod  16394  pythagtrip  16794  isstruct  17111  pgpfac1  20046  pgpfac  20050  basdif0  22927  ntreq0  23051  tgcmp  23375  tx1cn  23583  rnelfmlem  23926  phtpcer  24971  iscvsp  25104  caucfil  25259  minveclem1  25400  ovoliunlem1  25478  mdegleb  26041  eqcuts2  27797  dmcuts  27802  made0  27874  mulsuniflem  28160  istrkg2ld  28547  numedglnl  29232  usgr2pth0  29853  adjbd1o  32176  nmo  32579  dmrab  32586  difrab2  32587  mpomptxf  32771  ccfldextdgrr  33837  fldextrspunlsplem  33838  isros  34333  1stmbfm  34425  bnj976  34941  bnj1143  34953  bnj1533  35015  bnj864  35085  bnj983  35114  bnj1174  35166  bnj1175  35167  bnj1280  35183  axregs  35304  onvf1odlem2  35307  cvmlift2lem12  35517  axacprim  35910  dfrecs2  36153  andnand1  36604  bj-snglc  37289  bj-disj2r  37348  bj-dfmpoa  37443  bj-mpomptALT  37444  mptsnunlem  37665  wl-df3xor2  37796  wl-df4-3mintru2  37814  wl-cases2-dnf  37848  wl-euae  37853  itg2addnc  38006  asindmre  38035  brres2  38605  brxrn2  38716  dfxrn2  38717  inxpxrn  38750  dfsuccl4  38806  refsymrel2  38983  refsymrel3  38984  dfeqvrel2  39006  dfeqvrel3  39007  isopos  39637  dihglblem6  41797  dihglb2  41799  fgraphopab  43646  unielss  43661  dflim5  43772  ifpid2g  43935  ifpim23g  43937  rp-fakeanorass  43955  en2pr  43989  elmapintrab  44018  relnonrel  44029  undmrnresiss  44046  elintima  44095  relexp0eq  44143  iunrelexp0  44144  dffrege115  44420  frege131  44436  frege133  44438  ntrneikb  44536  elnev  44879  onfrALTlem5  44984  onfrALTlem5VD  45326  ndisj2  45497  ndmaovcom  47650  usgrexmpl2nb3  48507  eliunxp2  48807  mpomptx2  48808  mo0sn  49288  i0oii  49392  io1ii  49393  alimp-no-surprise  50253  alsi-no-surprise  50268