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 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  con2bi  356  xorneg2  1551  sbrimvwOLD  2126  2eu4  2682  2eu5  2683  r19.41v  3195  r3ex  3204  r19.41  3269  sbralie  3342  sbralieOLD  3344  pm13.183  3626  euxfrw  3685  euxfr  3687  euind  3688  rmo4  3694  rmo3f  3698  2reu5lem3  3721  rmo3  3843  difin  4226  indifdi  4248  dftr5  5223  axsepgfromrep  5256  inuni  5322  reusv2lem4  5374  rabxp  5711  elvvv  5739  eliunxp  5825  elidinxp  6048  imadisj  6084  idrefALT  6115  intirr  6120  resco  6253  funcnv3  6608  fncnv  6611  fun11  6612  fununi  6613  mptfnf  6672  f1mpt  7261  mpomptx  7525  uniuni  7762  frxp  8123  xpord2pred  8142  xpord2indlem  8144  oeeu  8590  ixp0x  8925  xpcomco  9056  dffi3  9392  wemapsolem  9513  cardval3  9939  kmlem4  10138  kmlem12  10146  kmlem14  10148  kmlem15  10149  kmlem16  10150  fpwwe2  10629  axgroth4  10818  ltexprlem4  11025  bitsmod  16495  pythagtrip  16895  isstruct  17213  pgpfac1  20153  pgpfac  20157  basdif0  23091  ntreq0  23215  tgcmp  23539  tx1cn  23747  rnelfmlem  24090  phtpcer  25135  iscvsp  25268  caucfil  25423  minveclem1  25564  ovoliunlem1  25642  mdegleb  26202  eqcuts2  27960  dmcuts  27965  made0  28037  mulsuniflem  28323  istrkg2ld  28710  numedglnl  29475  usgr2pth0  30095  adjbd1o  32418  nmo  32817  dmrab  32824  difrab2  32825  mpomptxf  33004  ccfldextdgrr  34043  fldextrspunlsplem  34044  isros  34539  1stmbfm  34631  bnj976  35147  bnj1143  35159  bnj1533  35221  bnj864  35291  bnj983  35320  bnj1174  35372  bnj1175  35373  bnj1280  35389  axregs  35533  onvf1odlem2  35569  cvmlift2lem12  35787  axacprim  36180  dfrecs2  36423  andnand1  36893  mh-infprim1bi  37038  bj-snglc  37586  bj-disj2r  37645  bj-dfmpoa  37741  bj-mpomptALT  37742  mptsnunlem  37965  wl-df3xor2  38096  wl-df4-3mintru2  38114  wl-cases2-dnf  38148  wl-euae  38153  itg2addnc  38306  asindmre  38335  brres2  38903  brxrn2  39014  dfxrn2  39015  inxpxrn  39048  dfsuccl4  39104  refsymrel2  39281  refsymrel3  39282  dfeqvrel2  39304  dfeqvrel3  39305  isopos  39935  dihglblem6  42095  dihglb2  42097  fgraphopab  43913  unielss  43928  dflim5  44039  ifpid2g  44202  ifpim23g  44204  rp-fakeanorass  44222  en2pr  44256  elmapintrab  44285  relnonrel  44296  undmrnresiss  44313  elintima  44362  relexp0eq  44410  iunrelexp0  44411  dffrege115  44687  frege131  44703  frege133  44705  ntrneikb  44803  elnev  45130  onfrALTlem5  45234  onfrALTlem5VD  45576  ndisj2  45754  ndmaovcom  47925  usgrexmpl2nb3  48782  eliunxp2  49097  mpomptx2  49098  mo0sn  49577  i0oii  49681  io1ii  49682  alimp-no-surprise  50542  als-no-surprise  50567