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 205

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 206

This theorem is referenced by:  con2bi  354  xorneg2  1521  sbrimvw  2095  2eu4  2651  2eu5  2652  sbralie  3355  euxfrw  3718  euxfr  3720  euind  3721  rmo4  3727  rmo3f  3731  2reu5lem3  3754  rmo3  3884  difin  4262  indifdi  4284  ab0orv  4379  dftr5  5270  axsepgfromrep  5298  reusv2lem4  5400  rabxp  5725  elvvv  5752  eliunxp  5838  elidinxp  6044  imadisj  6080  idrefALT  6113  intirr  6120  resco  6250  funcnv3  6619  fncnv  6622  fun11  6623  fununi  6624  mptfnf  6686  f1mpt  7260  mpomptx  7521  uniuni  7749  frxp  8112  xpord2pred  8131  xpord2indlem  8133  oeeu  8603  ixp0x  8920  xpcomco  9062  1sdomOLD  9249  dffi3  9426  wemapsolem  9545  cardval3  9947  kmlem4  10148  kmlem12  10156  kmlem14  10158  kmlem15  10159  kmlem16  10160  fpwwe2  10638  axgroth4  10827  ltexprlem4  11034  bitsmod  16377  pythagtrip  16767  isstruct  17085  pgpfac1  19950  pgpfac  19954  basdif0  22456  ntreq0  22581  tgcmp  22905  tx1cn  23113  rnelfmlem  23456  phtpcer  24511  iscvsp  24644  caucfil  24800  minveclem1  24941  ovoliunlem1  25019  mdegleb  25582  eqscut2  27307  dmscut  27312  made0  27368  mulsuniflem  27604  istrkg2ld  27711  numedglnl  28404  usgr2pth0  29022  adjbd1o  31338  nmo  31730  dmrab  31737  difrab2  31738  mpomptxf  31905  ccfldextdgrr  32746  isros  33166  1stmbfm  33259  bnj976  33788  bnj1143  33801  bnj1533  33863  bnj864  33933  bnj983  33962  bnj1174  34014  bnj1175  34015  bnj1280  34031  cvmlift2lem12  34305  axacprim  34676  dfrecs2  34922  andnand1  35286  bj-snglc  35850  bj-disj2r  35909  bj-dfmpoa  35999  bj-mpomptALT  36000  mptsnunlem  36219  wl-df3xor2  36350  wl-df4-3mintru2  36368  wl-cases2-dnf  36381  wl-euae  36386  itg2addnc  36542  asindmre  36571  brres2  37136  brxrn2  37245  dfxrn2  37246  inxpxrn  37265  refsymrel2  37437  refsymrel3  37438  dfeqvrel2  37460  dfeqvrel3  37461  isopos  38050  dihglblem6  40211  dihglb2  40213  fgraphopab  41952  unielss  41967  dflim5  42079  ifpid2g  42244  ifpim23g  42246  rp-fakeanorass  42264  en2pr  42298  elmapintrab  42327  relnonrel  42338  undmrnresiss  42355  elintima  42404  relexp0eq  42452  iunrelexp0  42453  dffrege115  42729  frege131  42745  frege133  42747  ntrneikb  42845  elnev  43197  onfrALTlem5  43303  onfrALTlem5VD  43646  ndisj2  43738  ndmaovcom  45913  eliunxp2  47009  mpomptx2  47010  mo0sn  47500  i0oii  47552  io1ii  47553  alimp-no-surprise  47828  alsi-no-surprise  47843