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  1521  sbrimvw  2092  2eu4  2648  2eu5  2649  r19.41v  3159  r3ex  3168  r19.41  3233  sbralie  3317  sbralieOLD  3319  pm13.183  3623  euxfrw  3683  euxfr  3685  euind  3686  rmo4  3692  rmo3f  3696  2reu5lem3  3719  rmo3  3843  difin  4225  indifdi  4247  ab0orv  4336  dftr5  5206  axsepgfromrep  5236  inuni  5292  reusv2lem4  5343  rabxp  5671  elvvv  5699  eliunxp  5784  elidinxp  5999  imadisj  6035  idrefALT  6066  intirr  6071  resco  6203  funcnv3  6556  fncnv  6559  fun11  6560  fununi  6561  mptfnf  6621  f1mpt  7202  mpomptx  7466  uniuni  7702  frxp  8066  xpord2pred  8085  xpord2indlem  8087  oeeu  8528  ixp0x  8860  xpcomco  8991  dffi3  9340  wemapsolem  9461  cardval3  9867  kmlem4  10067  kmlem12  10075  kmlem14  10077  kmlem15  10078  kmlem16  10079  fpwwe2  10556  axgroth4  10745  ltexprlem4  10952  bitsmod  16365  pythagtrip  16764  isstruct  17081  pgpfac1  19979  pgpfac  19983  basdif0  22856  ntreq0  22980  tgcmp  23304  tx1cn  23512  rnelfmlem  23855  phtpcer  24910  iscvsp  25044  caucfil  25199  minveclem1  25340  ovoliunlem1  25419  mdegleb  25985  eqscut2  27735  dmscut  27740  made0  27805  mulsuniflem  28075  istrkg2ld  28423  numedglnl  29107  usgr2pth0  29728  adjbd1o  32047  nmo  32452  dmrab  32459  difrab2  32460  mpomptxf  32634  ccfldextdgrr  33646  fldextrspunlsplem  33647  isros  34137  1stmbfm  34230  bnj976  34746  bnj1143  34759  bnj1533  34821  bnj864  34891  bnj983  34920  bnj1174  34972  bnj1175  34973  bnj1280  34989  axregs  35076  onvf1odlem2  35079  cvmlift2lem12  35289  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  38245  brxrn2  38345  dfxrn2  38346  inxpxrn  38369  refsymrel2  38546  refsymrel3  38547  dfeqvrel2  38569  dfeqvrel3  38570  isopos  39161  dihglblem6  41322  dihglb2  41324  fgraphopab  43179  unielss  43194  dflim5  43305  ifpid2g  43469  ifpim23g  43471  rp-fakeanorass  43489  en2pr  43523  elmapintrab  43552  relnonrel  43563  undmrnresiss  43580  elintima  43629  relexp0eq  43677  iunrelexp0  43678  dffrege115  43954  frege131  43970  frege133  43972  ntrneikb  44070  elnev  44414  onfrALTlem5  44519  onfrALTlem5VD  44861  ndisj2  45032  ndmaovcom  47193  usgrexmpl2nb3  48022  eliunxp2  48322  mpomptx2  48323  mo0sn  48804  i0oii  48908  io1ii  48909  alimp-no-surprise  49770  alsi-no-surprise  49785