Theorem 3bitr2i 301

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  con2bi  356  xorneg2  1512  sbrimvlem  2101  dfsb7OLD  2286  2eu4  2739  2eu5  2740  2eu5OLD  2741  euxfrw  3712  euxfr  3714  euind  3715  rmo4  3721  rmo3f  3725  2reu5lem3  3748  rmo3  3872  rmo3OLD  3873  difin  4238  axsepgfromrep  5201  reusv2lem4  5302  rabxp  5600  elvvv  5627  eliunxp  5708  elidinxp  5911  imadisj  5948  idrefALT  5973  intirr  5978  resco  6103  funcnv3  6424  fncnv  6427  fun11  6428  fununi  6429  mptfnf  6483  f1mpt  7019  mpomptx  7265  uniuni  7484  frxp  7820  oeeu  8229  ixp0x  8490  xpcomco  8607  1sdom  8721  dffi3  8895  wemapsolem  9014  cardval3  9381  kmlem4  9579  kmlem12  9587  kmlem14  9589  kmlem15  9590  kmlem16  9591  fpwwe2  10065  axgroth4  10254  ltexprlem4  10461  bitsmod  15785  pythagtrip  16171  isstruct  16496  pgpfac1  19202  pgpfac  19206  isassa  20088  basdif0  21561  ntreq0  21685  tgcmp  22009  tx1cn  22217  rnelfmlem  22560  phtpcer  23599  iscvsp  23732  caucfil  23886  minveclem1  24027  ovoliunlem1  24103  mdegleb  24658  istrkg2ld  26246  numedglnl  26929  usgr2pth0  27546  adjbd1o  29862  nelbOLD  30232  nmo  30254  dmrab  30260  difrab2  30261  mpomptxf  30425  ccfldextdgrr  31057  isros  31427  1stmbfm  31518  bnj976  32049  bnj1143  32062  bnj1533  32124  bnj864  32194  bnj983  32223  bnj1174  32275  bnj1175  32276  bnj1280  32292  cvmlift2lem12  32561  axacprim  32933  dmscut  33272  dfrecs2  33411  andnand1  33749  bj-snglc  34284  bj-disj2r  34343  bj-dfmpoa  34413  bj-mpomptALT  34414  mptsnunlem  34622  wl-cases2-dnf  34767  wl-euae  34772  wl-dfralv  34856  itg2addnc  34961  asindmre  34992  brres2  35544  brxrn2  35642  dfxrn2  35643  inxpxrn  35658  refsymrel2  35818  refsymrel3  35819  dfeqvrel2  35840  dfeqvrel3  35841  isopos  36331  dihglblem6  38491  dihglb2  38493  fgraphopab  39830  ifpid2g  39879  ifpim23g  39881  rp-fakeanorass  39899  en2pr  39926  elmapintrab  39956  relnonrel  39967  undmrnresiss  39984  elintima  40018  relexp0eq  40066  iunrelexp0  40067  dffrege115  40344  frege131  40360  frege133  40362  ntrneikb  40464  onfrALTlem5  40896  onfrALTlem5VD  41239  ndisj2  41333  ndmaovcom  43424  eliunxp2  44402  mpomptx2  44403  alimp-no-surprise  44902  alsi-no-surprise  44917