Theorem 3bitr4i 212

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 187	. 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:  bibi2d  232  pm4.71  389  pm5.32ri  455  mpan10  474  an31  564  an4  586  or4  772  ordir  818  andir  820  3anrot  985  3orrot  986  3ancoma  987  3orcomb  989  3ioran  995  3anbi123i  1190  3orbi123i  1191  3or6  1334  xorcom  1399  nfbii  1484  19.26-3an  1494  alnex  1510  19.42h  1698  19.42  1699  equsal  1738  equsalv  1804  sb6  1898  eeeanv  1945  sbbi  1971  sbco3xzyz  1985  sbcom2v  1997  sbel2x  2010  sb8eu  2051  sb8mo  2052  sb8euh  2061  eu1  2063  cbvmo  2078  mo3h  2091  sbmo  2097  eqcom  2191  abeq1  2299  cbvabw  2312  cbvab  2313  clelab  2315  nfceqi  2328  sbabel  2359  ralbii2  2500  rexbii2  2501  r2alf  2507  r2exf  2508  nfraldya  2525  nfrexdya  2526  r3al  2534  r19.41  2645  r19.42v  2647  ralcomf  2651  rexcomf  2652  reean  2659  3reeanv  2661  rabid2  2667  rabbi  2668  reubiia  2675  rmobiia  2680  reu5  2703  rmo5  2706  cbvralfw  2708  cbvrexfw  2709  cbvralf  2710  cbvrexf  2711  cbvreu  2716  cbvrmo  2717  cbvralvw  2722  cbvrexvw  2723  vjust  2753  ceqsex3v  2794  ceqsex4v  2795  ceqsex8v  2797  eueq  2923  reu2  2940  reu6  2941  reu3  2942  rmo4  2945  rmo3f  2949  2rmorex  2958  cbvsbcw  3005  cbvsbc  3006  sbccomlem  3052  rmo3  3069  csbcow  3083  csbabg  3133  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  eqss  3185  uniiunlem  3259  ssequn1  3320  unss  3324  rexun  3330  ralunb  3331  elin3  3341  incom  3342  inass  3360  ssin  3372  ssddif  3384  unssdif  3385  difin  3387  invdif  3392  indif  3393  indi  3397  symdifxor  3416  disj3  3490  eldifpr  3634  rexsns  3646  reusn  3678  prss  3763  tpss  3773  eluni2  3828  elunirab  3837  uniun  3843  uni0b  3849  unissb  3854  elintrab  3871  ssintrab  3882  intun  3890  intpr  3891  iuncom  3907  iuncom4  3908  iunab  3948  ssiinf  3951  iinab  3963  iunin2  3965  iunun  3980  iunxun  3981  iunxiun  3983  sspwuni  3986  iinpw  3992  cbvdisj  4005  brun  4069  brin  4070  brdif  4071  dftr2  4118  inuni  4173  repizf2lem  4179  unidif0  4185  ssext  4239  pweqb  4241  otth2  4259  opelopabsbALT  4277  eqopab2b  4297  pwin  4300  unisuc  4431  elpwpwel  4493  sucexb  4514  elomssom  4622  xpiundi  4702  xpiundir  4703  poinxp  4713  soinxp  4714  seinxp  4715  inopab  4777  difopab  4778  raliunxp  4786  rexiunxp  4787  iunxpf  4793  cnvco  4830  dmiun  4854  dmuni  4855  dm0rn0  4862  brres  4931  dmres  4946  restidsing  4981  cnvsym  5030  asymref  5032  codir  5035  qfto  5036  cnvopab  5048  cnvdif  5053  rniun  5057  dminss  5061  imainss  5062  cnvcnvsn  5123  resco  5151  imaco  5152  rnco  5153  coiun  5156  coass  5165  ressn  5187  cnviinm  5188  xpcom  5193  funcnv  5296  funcnv3  5297  fncnv  5301  fun11  5302  fnres  5351  dfmpt3  5357  fnopabg  5358  fintm  5420  fin  5421  fores  5466  dff1o3  5486  fun11iun  5501  f11o  5513  f1ompt  5688  fsn  5709  imaiun  5782  isores2  5835  eqoprab2b  5955  opabex3d  6147  opabex3  6148  dfopab2  6215  dfoprab3s  6216  fmpox  6226  tpostpos  6290  dfsmo2  6313  qsid  6627  mapval2  6705  mapsncnv  6722  elixp2  6729  ixpin  6750  xpassen  6857  diffitest  6916  pw1dc0el  6940  supmoti  7023  eqinfti  7050  distrnqg  7417  ltbtwnnq  7446  distrnq0  7489  nqprrnd  7573  ltresr  7869  elznn0nn  9298  xrnemnf  9809  xrnepnf  9810  elioomnf  10000  elxrge0  10010  elfzuzb  10051  fzass4  10094  elfz2nn0  10144  elfzo2  10182  elfzo3  10195  lbfzo0  10213  fzind2  10271  dfrp2  10296  rexfiuz  11033  fisumcom2  11481  prodmodc  11621  fprodcom2fi  11669  infssuzex  11985  4sqlem12  12437  infpn2  12510  xpsfrnel  12823  xpscf  12826  islmod  13624  isbasis2g  14022  tgval2  14028  ntreq0  14109  txuni2  14233  isms2  14431  bdceq  15072