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  763  orass  767  or32  770  dcan  933  dn1dc  960  an6  1321  excxor  1378  trubifal  1416  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  alrot4  1486  excom13  1689  sborv  1890  3exdistr  1915  4exdistr  1916  eeeanv  1933  ee4anv  1934  ee8anv  1935  sb3an  1958  sb9  1979  sbnf2  1981  sbco4  2007  2exsb  2009  sb8eu  2039  sb8euh  2049  sbmo  2085  2eu4  2119  2eu7  2120  elsb1  2155  elsb2  2156  r19.26-3  2607  rexcom13  2643  cbvreu  2702  ceqsex2  2778  ceqsex4v  2781  spc3gv  2831  ralrab2  2903  rexrab2  2905  reu2  2926  rmo4  2931  reu8  2934  rmo3f  2935  sbc3an  3025  rmo3  3055  dfss2  3145  ss2rab  3232  rabss  3233  ssrab  3234  dfdif3  3246  undi  3384  undif3ss  3397  difin2  3398  dfnul2  3425  disj  3472  disjsn  3655  snssb  3726  uni0c  3836  ssint  3861  iunss  3928  ssextss  4221  eqvinop  4244  opcom  4251  opeqsn  4253  opeqpr  4254  brabsb  4262  opelopabf  4275  opabm  4281  pofun  4313  sotritrieq  4326  uniuni  4452  ordsucim  4500  opeliunxp  4682  xpiundi  4685  brinxp2  4694  ssrel  4715  reliun  4748  cnvuni  4814  dmopab3  4841  opelres  4913  elres  4944  elsnres  4945  intirr  5016  ssrnres  5072  dminxp  5074  dfrel4v  5081  dmsnm  5095  rnco  5136  sb8iota  5186  dffun2  5227  dffun4f  5233  funco  5257  funcnveq  5280  fun11  5284  isarep1  5303  dff1o4  5470  dff1o6  5777  oprabid  5907  mpo2eqb  5984  ralrnmpo  5989  rexrnmpo  5990  opabex3d  6122  opabex3  6123  xporderlem  6232  f1od2  6236  tfr0dm  6323  tfrexlem  6335  frec0g  6398  nnaord  6510  ecid  6598  mptelixpg  6734  elixpsn  6735  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830  exmidontriimlem3  7222  nqnq0  7440  opelreal  7826  pitoregt0  7848  elnn0  9178  elxnn0  9241  elxr  9776  xrnepnf  9778  elfzuzb  10019  4fvwrd4  10140  elfzo2  10150  resqrexlemsqa  11033  fisumcom2  11446  modfsummod  11466  fprodcom2fi  11634  nnwosdc  12040  isprm2  12117  isprm4  12119  pythagtriplem2  12266  isnsg2  13063  isnsg4  13072  ntreq0  13635  txbas  13761  metrest  14009