Theorem 3bitr4ri 306

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 280	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 278	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  biadan  817  pm4.78  931  xor  1011  cases2  1042  noranOLD  1527  nic-ax  1674  2sb6  2094  2sb5  2282  dfsb7  2285  2sb5rf  2496  2sb6rf  2497  eu6lem  2658  eu6  2659  2mo2  2732  2eu7  2743  2eu8  2744  euae  2745  ralanidOLD  3169  r3al  3202  risset  3267  r2exlem  3302  ralxpxfr2d  3639  reuind  3744  undif3  4265  unab  4270  inab  4271  n0el  4321  inssdif0  4329  ssundif  4433  ralf0  4457  raldifsnb  4729  pwtp  4833  unipr  4855  uni0b  4864  iinuni  5020  reusv2lem4  5302  pwtr  5345  opthprc  5616  xpiundir  5623  xpsspw  5682  relun  5684  inopab  5701  difopab  5702  ralxpf  5717  dmiun  5782  elidinxp  5911  iresn0n0  5923  inisegn0  5961  rniun  6006  imaco  6104  rnco  6105  mptfnf  6483  fnopabg  6485  dff1o2  6620  brprcneu  6662  idref  6908  imaiun  7004  sorpss  7454  opabex3d  7666  opabex3rd  7667  opabex3  7668  ovmptss  7788  fnsuppres  7857  rankc1  9299  aceq1  9543  dfac10  9563  fin41  9866  axgroth6  10250  genpass  10431  infm3  11600  prime  12064  elixx3g  12752  elfz2  12900  elfzuzb  12903  rpnnen2lem12  15578  divalgb  15755  1nprm  16023  maxprmfct  16053  vdwmc  16314  imasleval  16814  issubm  17968  issubg3  18297  efgrelexlemb  18876  ist1-2  21955  unisngl  22135  elflim2  22572  isfcls  22617  istlm  22793  isnlm  23284  ishl2  23973  ovoliunlem1  24103  erclwwlkref  27798  erclwwlknref  27848  0wlk  27895  h1de2ctlem  29332  nonbooli  29428  5oalem7  29437  ho01i  29605  rnbra  29884  cvnbtwn3  30065  chrelat2i  30142  nelbOLD  30232  moel  30252  difrab2  30261  uniinn0  30302  disjex  30342  maprnin  30467  ordtconnlem1  31167  esum2dlem  31351  eulerpartgbij  31630  eulerpartlemr  31632  eulerpartlemn  31639  ballotlem2  31746  bnj976  32049  bnj1185  32065  bnj543  32165  bnj571  32178  bnj611  32190  bnj916  32205  bnj1000  32213  bnj1040  32244  iscvm  32506  untuni  32935  dfso3  32950  dffr5  32989  elima4  33019  brtxpsd3  33357  brbigcup  33359  fixcnv  33369  ellimits  33371  elfuns  33376  brimage  33387  brcart  33393  brimg  33398  brapply  33399  brcup  33400  brcap  33401  dfrdg4  33412  dfint3  33413  ellines  33613  elicc3  33665  bj-snsetex  34278  bj-snglc  34284  bj-projun  34309  bj-vjust  34349  wl-cases2-dnf  34767  poimirlem27  34934  mblfinlem2  34945  iscrngo2  35290  n0elqs  35598  inxpxrn  35658  eqvrelcoss3  35868  prtlem70  36008  prtlem100  36010  prtlem15  36026  prter2  36032  lcvnbtwn3  36179  ishlat1  36503  ishlat2  36504  hlrelat2  36554  islpln5  36686  islvol5  36730  pclclN  37042  cdleme0nex  37441  aaitgo  39782  isdomn3  39824  imaiun1  40016  relexp0eq  40066  ntrk1k3eqk13  40420  2sbc6g  40767  2sbc5g  40768  2reu7  43330  2reu8  43331  alsconv  44911