Theorem 3bitr2i 291

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 270	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 267	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  con2bi  345  an13  637  xorneg2  1592  2eu4  2685  2eu5  2686  euxfr  3604  euind  3605  rmo4  3611  rmo3f  3615  2reu5lem3  3632  rmo3  3745  rmo3OLD  3746  difin  4088  reusv2lem4  5113  rabxp  5400  elvvv  5424  eliunxp  5505  elidinxp  5705  imadisj  5738  idrefALT  5763  intirr  5769  resco  5893  funcnv3  6204  fncnv  6207  fun11  6208  fununi  6209  mptfnf  6261  f1mpt  6790  mpt2mptx  7028  uniuni  7248  frxp  7568  oeeu  7967  ixp0x  8222  xpcomco  8338  1sdom  8451  dffi3  8625  wemapsolem  8744  cardval3  9111  kmlem4  9310  kmlem12  9318  kmlem14  9320  kmlem15  9321  kmlem16  9322  fpwwe2  9800  axgroth4  9989  ltexprlem4  10196  bitsmod  15564  pythagtrip  15943  isstruct  16268  pgpfac1  18866  pgpfac  18870  isassa  19712  basdif0  21165  ntreq0  21289  tgcmp  21613  tx1cn  21821  rnelfmlem  22164  phtpcer  23202  iscvsp  23335  caucfil  23489  minveclem1  23630  ovoliunlem1  23706  mdegleb  24261  istrkg2ld  25811  numedglnl  26493  usgr2pth0  27117  adjbd1o  29516  nmo  29897  difrab2  29901  mpt2mptxf  30043  isros  30829  1stmbfm  30920  bnj976  31447  bnj1143  31460  bnj1533  31521  bnj864  31591  bnj983  31620  bnj1174  31670  bnj1175  31671  bnj1280  31687  cvmlift2lem12  31895  axacprim  32181  dmscut  32507  dfrecs2  32646  andnand1  32984  bj-dfssb2  33230  bj-denotes  33427  bj-snglc  33529  bj-disj2r  33585  bj-dfmpt2a  33644  bj-mpt2mptALT  33645  mptsnunlem  33781  wl-cases2-dnf  33890  wl-euae  33895  wl-dfralv  33980  itg2addnc  34091  asindmre  34122  brres2  34669  brxrn2  34767  dfxrn2  34768  inxpxrn  34783  refsymrel2  34943  refsymrel3  34944  dfeqvrel2  34964  dfeqvrel3  34965  isopos  35336  dihglblem6  37496  dihglb2  37498  fgraphopab  38751  ifpid2g  38800  ifpim23g  38802  rp-fakeanorass  38820  elmapintrab  38843  relintabex  38848  relnonrel  38854  undmrnresiss  38871  elintima  38906  relexp0eq  38954  iunrelexp0  38955  dffrege115  39232  frege131  39248  frege133  39250  ntrneikb  39352  onfrALTlem5  39706  onfrALTlem5VD  40058  ndisj2  40154  ndmaovcom  42250  eliunxp2  43131  mpt2mptx2  43132  alimp-no-surprise  43637  alsi-no-surprise  43652