Theorem 3bitr4ri 291

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

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

Assertion

Ref	Expression
3bitr4ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 265	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 263	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 195

This theorem is referenced by:  pm4.78  603  xor  930  nannan  1442  nic-ax  1588  2sb5  2430  2sb6  2431  2sb5rf  2438  moabs  2488  2mo2  2537  2eu7  2546  2eu8  2547  r3al  2923  r2exlem  3040  risset  3043  r19.35  3064  ralxpxfr2d  3297  reuind  3377  undif3  3846  undif3OLD  3847  unab  3852  inab  3853  inssdif0  3900  ssundif  4003  ralf0  4029  snss  4258  raldifsnb  4265  pwtp  4363  unipr  4379  uni0b  4393  iinuni  4539  reusv2lem4  4793  pwtr  4842  elxp2OLD  5047  opthprc  5079  xpiundir  5087  xpsspw  5145  relun  5147  inopab  5162  difopab  5163  ralxpf  5178  dmiun  5242  inisegn0  5403  rniun  5448  imaco  5543  mptfnf  5914  fnopabg  5916  dff1o2  6040  brprcneu  6081  idref  6381  imaiun  6385  sorpss  6817  opabex3d  7014  opabex3  7015  ovmptss  7122  fnsuppres  7186  rankc1  8593  aceq1  8800  dfac10  8819  fin41  9126  axgroth6  9506  genpass  9687  infm3  10831  prime  11290  elixx3g  12015  elfz2  12159  elfzuzb  12162  rpnnen2lem12  14739  divalgb  14911  1nprm  15176  maxprmfct  15205  vdwmc  15466  imasleval  15970  issubm  17116  issubg3  17381  efgrelexlemb  17932  ist1-2  20903  unisngl  21082  elflim2  21520  isfcls  21565  istlm  21740  isnlm  22222  ishl2  22891  0wlk  25841  0trl  25842  erclwwlkref  26107  erclwwlknref  26119  h1de2ctlem  27604  nonbooli  27700  5oalem7  27709  ho01i  27877  rnbra  28156  cvnbtwn3  28337  chrelat2i  28414  moel  28513  uniinn0  28555  disjex  28593  maprnin  28700  ordtconlem1  29104  esum2dlem  29287  eulerpartgbij  29567  eulerpartlemr  29569  eulerpartlemn  29576  ballotlem2  29683  bnj976  29908  bnj1185  29924  bnj543  30023  bnj571  30036  bnj611  30048  bnj916  30063  bnj1000  30071  bnj1040  30100  iscvm  30301  untuni  30646  dfso3  30662  dffr5  30702  elima4  30730  nofulllem5  30911  brtxpsd3  30979  brbigcup  30981  fixcnv  30991  ellimits  30993  elfuns  30998  brimage  31009  brcart  31015  brimg  31020  brapply  31021  brcup  31022  brcap  31023  dfrdg4  31034  dfint3  31035  ellines  31235  elicc3  31287  bj-ssb1  31628  bj-snsetex  31940  bj-snglc  31946  bj-projun  31971  bj-vjust2  32002  wl-cases2-dnf  32270  poimirlem27  32402  mblfinlem2  32413  iscrngo2  32762  prtlem70  32953  prtlem100  32957  n0el  32960  prtlem15  32974  prter2  32980  lcvnbtwn3  33129  ishlat1  33453  ishlat2  33454  hlrelat2  33503  islpln5  33635  islvol5  33679  pclclN  33991  cdleme0nex  34391  aaitgo  36547  isdomn3  36597  imaiun1  36758  relexp0eq  36808  ntrk1k3eqk13  37164  2sbc6g  37434  2sbc5g  37435  2reu7  39637  2reu8  39638  erclwwlksref  41236  erclwwlksnref  41248  01wlk  41279  alsconv  42301