Theorem 3bitr2i 298

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 277	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 274	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  353  xorneg2  1514  sbrimvlem  2095  2eu4  2656  2eu5  2657  euxfrw  3651  euxfr  3653  euind  3654  rmo4  3660  rmo3f  3664  2reu5lem3  3687  rmo3  3818  difin  4192  indifdi  4214  ab0orv  4309  axsepgfromrep  5216  reusv2lem4  5319  rabxp  5626  elvvv  5653  eliunxp  5735  elidinxp  5940  imadisj  5977  idrefALT  6007  intirr  6012  resco  6143  funcnv3  6488  fncnv  6491  fun11  6492  fununi  6493  mptfnf  6552  f1mpt  7115  mpomptx  7365  uniuni  7590  frxp  7938  oeeu  8396  ixp0x  8672  xpcomco  8802  1sdom  8955  dffi3  9120  wemapsolem  9239  cardval3  9641  kmlem4  9840  kmlem12  9848  kmlem14  9850  kmlem15  9851  kmlem16  9852  fpwwe2  10330  axgroth4  10519  ltexprlem4  10726  bitsmod  16071  pythagtrip  16463  isstruct  16781  pgpfac1  19598  pgpfac  19602  isassa  20973  basdif0  22011  ntreq0  22136  tgcmp  22460  tx1cn  22668  rnelfmlem  23011  phtpcer  24064  iscvsp  24197  caucfil  24352  minveclem1  24493  ovoliunlem1  24571  mdegleb  25134  istrkg2ld  26725  numedglnl  27417  usgr2pth0  28034  adjbd1o  30348  nelbOLDOLD  30718  nmo  30739  dmrab  30745  difrab2  30746  mpomptxf  30918  ccfldextdgrr  31644  isros  32036  1stmbfm  32127  bnj976  32657  bnj1143  32670  bnj1533  32732  bnj864  32802  bnj983  32831  bnj1174  32883  bnj1175  32884  bnj1280  32900  cvmlift2lem12  33176  axacprim  33548  xpord2pred  33719  xpord2ind  33721  eqscut2  33927  dmscut  33932  made0  33984  dfrecs2  34179  andnand1  34517  bj-snglc  35086  bj-disj2r  35145  bj-dfmpoa  35216  bj-mpomptALT  35217  mptsnunlem  35436  wl-df3xor2  35567  wl-df4-3mintru2  35585  wl-cases2-dnf  35598  wl-euae  35603  itg2addnc  35758  asindmre  35787  brres2  36334  brxrn2  36432  dfxrn2  36433  inxpxrn  36448  refsymrel2  36608  refsymrel3  36609  dfeqvrel2  36630  dfeqvrel3  36631  isopos  37121  dihglblem6  39281  dihglb2  39283  fgraphopab  40951  ifpid2g  40998  ifpim23g  41000  rp-fakeanorass  41018  en2pr  41043  elmapintrab  41073  relnonrel  41084  undmrnresiss  41101  elintima  41150  relexp0eq  41198  iunrelexp0  41199  dffrege115  41475  frege131  41491  frege133  41493  ntrneikb  41593  onfrALTlem5  42051  onfrALTlem5VD  42394  ndisj2  42488  ndmaovcom  44584  eliunxp2  45557  mpomptx2  45558  mo0sn  46049  i0oii  46101  io1ii  46102  alimp-no-surprise  46371  alsi-no-surprise  46386