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  1522  sbrimvw  2096  2eu4  2652  2eu5  2653  r19.41v  3163  r3ex  3172  r19.41  3237  sbralie  3319  sbralieOLD  3321  pm13.183  3617  euxfrw  3676  euxfr  3678  euind  3679  rmo4  3685  rmo3f  3689  2reu5lem3  3712  rmo3  3836  difin  4221  indifdi  4243  dftr5  5204  axsepgfromrep  5234  inuni  5290  reusv2lem4  5341  rabxp  5667  elvvv  5695  eliunxp  5781  elidinxp  5997  imadisj  6033  idrefALT  6064  intirr  6069  resco  6202  funcnv3  6556  fncnv  6559  fun11  6560  fununi  6561  mptfnf  6621  f1mpt  7201  mpomptx  7465  uniuni  7701  frxp  8062  xpord2pred  8081  xpord2indlem  8083  oeeu  8524  ixp0x  8856  xpcomco  8987  dffi3  9322  wemapsolem  9443  cardval3  9852  kmlem4  10052  kmlem12  10060  kmlem14  10062  kmlem15  10063  kmlem16  10064  fpwwe2  10541  axgroth4  10730  ltexprlem4  10937  bitsmod  16349  pythagtrip  16748  isstruct  17065  pgpfac1  19996  pgpfac  20000  basdif0  22869  ntreq0  22993  tgcmp  23317  tx1cn  23525  rnelfmlem  23868  phtpcer  24922  iscvsp  25056  caucfil  25211  minveclem1  25352  ovoliunlem1  25431  mdegleb  25997  eqscut2  27748  dmscut  27753  made0  27819  mulsuniflem  28089  istrkg2ld  28439  numedglnl  29124  usgr2pth0  29745  adjbd1o  32067  nmo  32471  dmrab  32478  difrab2  32479  mpomptxf  32663  ccfldextdgrr  33706  fldextrspunlsplem  33707  isros  34202  1stmbfm  34294  bnj976  34810  bnj1143  34823  bnj1533  34885  bnj864  34955  bnj983  34984  bnj1174  35036  bnj1175  35037  bnj1280  35053  axregs  35166  onvf1odlem2  35169  cvmlift2lem12  35379  axacprim  35772  dfrecs2  36015  andnand1  36466  bj-snglc  37034  bj-disj2r  37093  bj-dfmpoa  37183  bj-mpomptALT  37184  mptsnunlem  37403  wl-df3xor2  37534  wl-df4-3mintru2  37552  wl-cases2-dnf  37577  wl-euae  37582  itg2addnc  37735  asindmre  37764  brres2  38326  brxrn2  38429  dfxrn2  38430  inxpxrn  38463  dfsuccl4  38508  refsymrel2  38684  refsymrel3  38685  dfeqvrel2  38707  dfeqvrel3  38708  isopos  39300  dihglblem6  41460  dihglb2  41462  fgraphopab  43321  unielss  43336  dflim5  43447  ifpid2g  43611  ifpim23g  43613  rp-fakeanorass  43631  en2pr  43665  elmapintrab  43694  relnonrel  43705  undmrnresiss  43722  elintima  43771  relexp0eq  43819  iunrelexp0  43820  dffrege115  44096  frege131  44112  frege133  44114  ntrneikb  44212  elnev  44555  onfrALTlem5  44660  onfrALTlem5VD  45002  ndisj2  45173  ndmaovcom  47330  usgrexmpl2nb3  48159  eliunxp2  48459  mpomptx2  48460  mo0sn  48941  i0oii  49045  io1ii  49046  alimp-no-surprise  49907  alsi-no-surprise  49922