Theorem 3bitri 206

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitri.1	⊢ (𝜑 ↔ 𝜓)
3bitri.2	⊢ (𝜓 ↔ 𝜒)
3bitri.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitri	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		3bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3		3bitri.3	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	2, 3	bitri 184	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 184	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bibi1i  228  an32  568  orbi1i  775  orass  779  or32  782  dn1dc  973  an6  1362  excxor  1427  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  alrot4  1539  excom13  1741  sborv  1945  3exdistr  1971  4exdistr  1972  eeeanv  1993  ee4anv  1994  ee8anv  1995  sb3an  2018  sb9  2039  sbnf2  2041  sbco4  2067  2exsb  2069  sb8eu  2099  sb8euh  2109  sbmo  2146  2eu4  2180  2eu7  2181  elsb1  2216  elsb2  2217  r19.26-3  2681  rexcom13  2717  cbvreu  2784  ceqsex2  2863  ceqsex4v  2866  spc3gv  2918  ralrab2  2991  rexrab2  2993  reu2  3014  rmo4  3019  reu8  3022  rmo3f  3023  sbc3an  3113  reu8nf  3133  rmo3  3144  ssalel  3235  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  undi  3479  undif3ss  3492  difin2  3493  disj  3573  disjsn  3770  snssb  3846  uni0c  3959  ssint  3984  iunss  4051  ssextss  4358  eqvinop  4381  opcom  4389  opeqsn  4391  opeqpr  4392  brabsb  4401  opelopabf  4415  opabm  4421  pofun  4455  sotritrieq  4468  uniuni  4595  ordsucim  4645  opeliunxp  4828  xpiundi  4831  brinxp2  4840  ssrel  4861  reliun  4896  cnvuni  4964  dmopab3  4992  opelres  5066  elres  5097  elsnres  5098  intirr  5172  ssrnres  5228  dminxp  5230  dfrel4v  5237  dmsnm  5251  rnco  5292  sb8iota  5343  dffun2  5385  dffun4f  5391  funco  5415  funcnveq  5442  fun11  5446  isarep1  5465  dff1o4  5645  dff1o6  5976  oprabid  6111  mpo2eqb  6192  ralrnmpo  6197  rexrnmpo  6198  opabex3d  6344  opabex3  6345  xporderlem  6461  f1od2  6465  tfr0dm  6587  tfrexlem  6599  frec0g  6662  nnaord  6776  ecid  6866  mptelixpg  7010  elixpsn  7011  mapsnen  7094  xpsnen  7113  xpcomco  7118  xpassen  7122  exmidontriimlem3  7573  nqnq0  7802  opelreal  8188  pitoregt0  8210  elnn0  9548  elxnn0  9615  elxr  10161  xrnepnf  10163  elfzuzb  10405  4fvwrd4  10530  elfzo2  10540  swrdnd  11414  resqrexlemsqa  11773  fisumcom2  12188  modfsummod  12208  fprodcom2fi  12376  nnwosdc  12799  isprm2  12878  isprm4  12880  pythagtriplem2  13028  4sqlem12  13164  isnsg2  13989  isnsg4  13998  dfrhm2  14444  cnfldui  14907  isassa  14985  ntreq0  15216  txbas  15342  metrest  15590  2lgslem4  16205  umgr2edg1  16433  isclwwlk  16618  isclwwlknx  16640  clwwlkn1  16642  clwwlkn2  16645  clwwlknonel  16656  iseupthf1o  16672  alsanmo  17125  ralsanmo  17126