Theorem 3bitr2i 302

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con2bi  356  xorneg2  1551  sbrimvwOLD  2129  2eu4  2680  2eu5  2681  r19.41v  3193  r3ex  3202  r19.41  3267  sbralie  3339  sbralieOLD  3341  pm13.183  3620  euxfrw  3679  euxfr  3681  euind  3682  rmo4  3688  rmo3f  3692  2reu5lem3  3715  rmo3  3836  difin  4218  indifdi  4240  dftr5  5216  axsepgfromrep  5247  inuni  5311  reusv2lem4  5363  rabxp  5699  elvvv  5727  eliunxp  5814  elidinxp  6038  imadisj  6074  idrefALT  6105  intirr  6110  resco  6244  funcnv3  6602  fncnv  6605  fun11  6606  fununi  6607  mptfnf  6666  f1mpt  7257  mpomptx  7525  mpt3mpt  7677  uniuni  7765  frxp  8127  xpord2pred  8146  xpord2indlem  8148  oeeu  8596  ixp0x  8938  xpcomco  9070  dffi3  9407  wemapsolem  9528  karden  9940  cardval3  10014  kmlem4  10213  kmlem12  10221  kmlem14  10223  kmlem15  10224  kmlem16  10225  fpwwe2  10709  axgroth4  10898  ltexprlem4  11105  bitsmod  16586  pythagtrip  16992  isstruct  17310  pgpfac1  20276  pgpfac  20280  basdif0  23251  ntreq0  23375  tgcmp  23699  tx1cn  23908  rnelfmlem  24251  phtpcer  25296  iscvsp  25429  caucfil  25584  minveclem1  25725  ovoliunlem1  25803  mdegleb  26362  eqcuts2  28154  dmcuts  28159  made0  28231  mulsuniflem  28517  istrkg2ld  28904  numedglnl  29704  usgr2pth0  30333  adjbd1o  32669  nmo  33068  dmrab  33075  difrab2  33076  mpomptxf  33254  ccfldextdgrr  34286  fldextrspunlsplem  34287  isros  34783  1stmbfm  34875  bnj976  35391  bnj1143  35403  bnj1533  35465  bnj864  35535  bnj983  35564  bnj1174  35616  bnj1175  35617  bnj1280  35633  axregs  35780  onvf1odlem2  35856  cvmlift2lem12  36048  axacprim  36441  dfrecs2  36684  andnand1  37159  mh-infprim1bi  37304  bj-snglc  37852  bj-disj2r  37911  bj-dfmpoa  38007  bj-mpomptALT  38008  mptsnunlem  38229  wl-df3xor2  38360  wl-df4-3mintru2  38378  wl-cases2-dnf  38412  wl-euae  38417  itg2addnc  38560  asindmre  38589  brres2  39173  brxrn2  39284  dfxrn2  39285  inxpxrn  39318  dfsuccl4  39374  refsymrel2  39551  refsymrel3  39552  dfeqvrel2  39574  dfeqvrel3  39575  isopos  40205  dihglblem6  42365  dihglb2  42367  fgraphopab  44163  unielss  44178  dflim5  44289  ifpid2g  44452  ifpim23g  44454  rp-fakeanorass  44472  en2pr  44506  elmapintrab  44535  relnonrel  44546  undmrnresiss  44563  elintima  44612  relexp0eq  44660  iunrelexp0  44661  dffrege115  44937  frege131  44953  frege133  44955  ntrneikb  45053  elnev  45380  onfrALTlem5  45484  onfrALTlem5VD  45826  ndisj2  46011  ndmaovcom  48219  usgrexmpl2nb3  49076  eliunxp2  49390  mpomptx2  49391  mo0sn  49870  i0oii  49972  io1ii  49973  alimp-no-surprise  50821  als-no-surprise  50846