Theorem 3bitr2i 287

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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  con2bi  342  an13  836  xorneg2  1466  2eu4  2544  2eu5  2545  exists1  2549  euxfr  3359  euind  3360  rmo4  3366  2reu5lem3  3382  rmo3  3494  difin  3823  reusv2lem4  4798  rabxp  5078  elvvv  5101  eliunxp  5181  imadisj  5403  intirr  5433  resco  5556  funcnv3  5873  fncnv  5876  fun11  5877  fununi  5878  mptfnf  5928  f1mpt  6419  mpt2mptx  6649  uniuni  6865  frxp  7174  oeeu  7570  ixp0x  7822  mapsnen  7920  xpcomco  7935  1sdom  8048  dffi3  8220  wemapsolem  8338  cardval3  8661  kmlem4  8858  kmlem12  8866  kmlem14  8868  kmlem15  8869  kmlem16  8870  fpwwe2  9344  axgroth4  9533  ltexprlem4  9740  bitsmod  14996  pythagtrip  15377  pgpfac1  18302  pgpfac  18306  isassa  19136  basdif0  20568  ntreq0  20691  tgcmp  21014  tx1cn  21222  rnelfmlem  21566  phtpcer  22602  phtpcerOLD  22603  iscvsp  22736  caucfil  22889  minveclem1  23003  ovoliunlem1  23077  mdegleb  23628  istrkg2ld  25159  3v3e3cycl2  26192  iswwlk  26211  adjbd1o  28328  nmo  28709  rmo3f  28719  rmo4fOLD  28720  mpt2mptxf  28860  isros  29558  1stmbfm  29649  bnj976  30102  bnj1143  30115  bnj1533  30176  bnj864  30246  bnj983  30275  bnj1174  30325  bnj1175  30326  bnj1280  30342  cvmlift2lem12  30550  axacprim  30838  dfrecs2  31227  andnand1  31568  bj-dfssb2  31829  bj-denotes  32052  bj-snglc  32150  bj-dfmpt2a  32252  bj-mpt2mptALT  32253  mptsnunlem  32361  wl-cases2-dnf  32474  itg2addnc  32634  asindmre  32665  isopos  33485  dihglblem6  35647  dihglb2  35649  fgraphopab  36807  ifpid2g  36857  ifpim23g  36859  rp-fakeanorass  36877  elmapintrab  36901  relintabex  36906  relnonrel  36912  undmrnresiss  36929  elintima  36964  relexp0eq  37012  iunrelexp0  37013  dffrege115  37292  frege131  37308  frege133  37310  ntrneikb  37412  onfrALTlem5  37778  ndisj2  38243  ndmaovcom  39934  usgr2pth0  40971  eliunxp2  41905  mpt2mptx2  41906  alimp-no-surprise  42336  alsi-no-surprise  42351