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  562  orbi1i  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2841  ceqsex4v  2844  spc3gv  2896  ralrab2  2968  rexrab2  2970  reu2  2991  rmo4  2996  reu8  2999  rmo3f  3000  sbc3an  3090  reu8nf  3110  rmo3  3121  ssalel  3212  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  undi  3452  undif3ss  3465  difin2  3466  dfnul2  3493  disj  3540  disjsn  3728  snssb  3801  uni0c  3914  ssint  3939  iunss  4006  ssextss  4307  eqvinop  4330  opcom  4338  opeqsn  4340  opeqpr  4341  brabsb  4350  opelopabf  4364  opabm  4370  pofun  4404  sotritrieq  4417  uniuni  4543  ordsucim  4593  opeliunxp  4776  xpiundi  4779  brinxp2  4788  ssrel  4809  reliun  4843  cnvuni  4911  dmopab3  4939  opelres  5013  elres  5044  elsnres  5045  intirr  5118  ssrnres  5174  dminxp  5176  dfrel4v  5183  dmsnm  5197  rnco  5238  sb8iota  5289  dffun2  5331  dffun4f  5337  funco  5361  funcnveq  5387  fun11  5391  isarep1  5410  dff1o4  5585  dff1o6  5909  oprabid  6042  mpo2eqb  6123  ralrnmpo  6128  rexrnmpo  6129  opabex3d  6275  opabex3  6276  xporderlem  6388  f1od2  6392  tfr0dm  6479  tfrexlem  6491  frec0g  6554  nnaord  6668  ecid  6758  mptelixpg  6894  elixpsn  6895  mapsnen  6977  xpsnen  6993  xpcomco  6998  xpassen  7002  exmidontriimlem3  7421  nqnq0  7644  opelreal  8030  pitoregt0  8052  elnn0  9387  elxnn0  9450  elxr  9989  xrnepnf  9991  elfzuzb  10232  4fvwrd4  10353  elfzo2  10363  swrdnd  11212  resqrexlemsqa  11556  fisumcom2  11970  modfsummod  11990  fprodcom2fi  12158  nnwosdc  12581  isprm2  12660  isprm4  12662  pythagtriplem2  12810  4sqlem12  12946  isnsg2  13761  isnsg4  13770  dfrhm2  14139  cnfldui  14574  ntreq0  14827  txbas  14953  metrest  15201  2lgslem4  15803  umgr2edg1  16028  isclwwlk  16163  isclwwlknx  16184  clwwlkn1  16186  clwwlkn2  16189