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  773  ordir  819  andir  821  3anrot  986  3orrot  987  3ancoma  988  3orcomb  990  3ioran  996  3anbi123i  1191  3orbi123i  1192  3or6  1336  xorcom  1408  nfbii  1497  19.26-3an  1507  alnex  1523  19.42h  1711  19.42  1712  equsal  1751  equsalv  1817  sb6  1911  eeeanv  1962  sbbi  1988  sbco3xzyz  2002  sbcom2v  2014  sbel2x  2027  sb8eu  2068  sb8mo  2069  sb8euh  2078  eu1  2080  cbvmo  2095  mo3h  2108  sbmo  2114  eqcom  2208  abeq1  2316  cbvabw  2329  cbvab  2330  clelab  2332  nfceqi  2345  sbabel  2376  ralbii2  2517  rexbii2  2518  r2alf  2524  r2exf  2525  nfraldya  2542  nfrexdya  2543  r3al  2551  r19.41  2662  r19.42v  2664  ralcomf  2668  rexcomf  2669  reean  2676  3reeanv  2678  rabid2  2684  rabbi  2685  reubiia  2692  rmobiia  2697  reu5  2724  rmo5  2727  cbvralfw  2729  cbvrexfw  2730  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvrmo  2738  cbvralvw  2743  cbvrexvw  2744  vjust  2774  ceqsex3v  2817  ceqsex4v  2818  ceqsex8v  2820  eueq  2948  reu2  2965  reu6  2966  reu3  2967  rmo4  2970  rmo3f  2974  2rmorex  2983  cbvsbcw  3030  cbvsbc  3031  sbccomlem  3077  rmo3  3094  csbcow  3108  csbabg  3159  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  eqss  3212  uniiunlem  3286  ssequn1  3347  unss  3351  rexun  3357  ralunb  3358  elin3  3368  incom  3369  inass  3387  ssin  3399  ssddif  3411  unssdif  3412  difin  3414  invdif  3419  indif  3420  indi  3424  symdifxor  3443  disj3  3517  eldifpr  3665  rexsns  3677  reusn  3709  prss  3795  tpss  3805  eluni2  3860  elunirab  3869  uniun  3875  uni0b  3881  unissb  3886  elintrab  3903  ssintrab  3914  intun  3922  intpr  3923  iuncom  3939  iuncom4  3940  iunab  3980  ssiinf  3983  iinab  3995  iunin2  3997  iunun  4012  iunxun  4013  iunxiun  4015  sspwuni  4018  iinpw  4024  cbvdisj  4037  brun  4103  brin  4104  brdif  4105  dftr2  4152  inuni  4207  repizf2lem  4213  unidif0  4219  ssext  4273  pweqb  4275  otth2  4293  opelopabsbALT  4313  eqopab2b  4334  pwin  4337  unisuc  4468  elpwpwel  4530  sucexb  4553  elomssom  4661  xpiundi  4741  xpiundir  4742  poinxp  4752  soinxp  4753  seinxp  4754  inopab  4818  difopab  4819  raliunxp  4827  rexiunxp  4828  iunxpf  4834  cnvco  4871  dmiun  4896  dmuni  4897  dm0rn0  4904  brres  4974  dmres  4989  restidsing  5024  cnvsym  5075  asymref  5077  codir  5080  qfto  5081  cnvopab  5093  cnvdif  5098  rniun  5102  dminss  5106  imainss  5107  cnvcnvsn  5168  resco  5196  imaco  5197  rnco  5198  coiun  5201  coass  5210  ressn  5232  cnviinm  5233  xpcom  5238  funcnv  5344  funcnv3  5345  fncnv  5349  fun11  5350  fnres  5402  dfmpt3  5408  fnopabg  5409  fintm  5473  fin  5474  fores  5520  dff1o3  5540  fun11iun  5555  f11o  5567  f1ompt  5744  fsn  5765  imaiun  5842  isores2  5895  eqoprab2b  6016  opabex3d  6219  opabex3  6220  dfopab2  6288  dfoprab3s  6289  fmpox  6299  tpostpos  6363  dfsmo2  6386  qsid  6700  mapval2  6778  mapsncnv  6795  elixp2  6802  ixpin  6823  xpassen  6940  diffitest  6999  pw1dc0el  7023  supmoti  7110  eqinfti  7137  distrnqg  7520  ltbtwnnq  7549  distrnq0  7592  nqprrnd  7676  ltresr  7972  elznn0nn  9406  xrnemnf  9919  xrnepnf  9920  elioomnf  10110  elxrge0  10120  elfzuzb  10161  fzass4  10204  elfz2nn0  10254  elfzo2  10292  elfzo3  10306  lbfzo0  10327  fzind2  10390  infssuzex  10398  dfrp2  10428  rexfiuz  11375  fisumcom2  11824  prodmodc  11964  fprodcom2fi  12012  4sqlem12  12800  infpn2  12902  xpsfrnel  13251  xpscf  13254  islmod  14128  isbasis2g  14592  tgval2  14598  ntreq0  14679  txuni2  14803  isms2  15001  plyun0  15283  bdceq  15916