Theorem 3bitr4ri 295

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

Syntax hints:   ↔ wb 197

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 198

This theorem is referenced by:  pm4.78  949  xor  1029  cases2  1061  nannan  1605  nic-ax  1753  2sb5  2288  2sb6  2289  2sb5rf  2611  moabs  2664  2mo2  2714  2eu7  2723  2eu8  2724  ralanid  3106  r3al  3128  r2exlem  3247  risset  3250  r19.35  3272  ralxpxfr2d  3521  reuind  3609  undif3  4090  unab  4095  inab  4096  n0el  4141  inssdif0  4148  ssundif  4248  ralf0  4272  raldifsnb  4517  pwtp  4625  unipr  4643  uni0b  4657  iinuni  4801  reusv2lem4  5070  pwtr  5111  opthprc  5367  xpiundir  5374  xpsspw  5434  relun  5436  inopab  5454  difopab  5455  ralxpf  5470  dmiun  5534  elidinxp  5660  inisegn0  5707  rniun  5754  imaco  5854  mptfnf  6226  fnopabg  6228  dff1o2  6358  brprcneu  6400  idref  6635  imaiun  6727  sorpss  7172  opabex3d  7375  opabex3  7376  ovmptss  7492  fnsuppres  7557  rankc1  8980  aceq1  9223  dfac10  9244  fin41  9551  axgroth6  9935  genpass  10116  infm3  11267  prime  11724  elixx3g  12406  elfz2  12556  elfzuzb  12559  rpnnen2lem12  15174  divalgb  15347  1nprm  15610  maxprmfct  15638  vdwmc  15899  imasleval  16406  issubm  17552  issubg3  17814  efgrelexlemb  18364  ist1-2  21365  unisngl  21544  elflim2  21981  isfcls  22026  istlm  22201  isnlm  22692  ishl2  23378  erclwwlkref  27163  erclwwlknref  27220  0wlk  27289  h1de2ctlem  28742  nonbooli  28838  5oalem7  28847  ho01i  29015  rnbra  29294  cvnbtwn3  29475  chrelat2i  29552  moel  29651  difrab2  29664  uniinn0  29691  disjex  29730  maprnin  29833  ordtconnlem1  30295  esum2dlem  30479  eulerpartgbij  30759  eulerpartlemr  30761  eulerpartlemn  30768  ballotlem2  30875  bnj976  31171  bnj1185  31187  bnj543  31286  bnj571  31299  bnj611  31311  bnj916  31326  bnj1000  31334  bnj1040  31363  iscvm  31564  untuni  31908  dfso3  31923  dffr5  31965  elima4  31999  brtxpsd3  32324  brbigcup  32326  fixcnv  32336  ellimits  32338  elfuns  32343  brimage  32354  brcart  32360  brimg  32365  brapply  32366  brcup  32367  brcap  32368  dfrdg4  32379  dfint3  32380  ellines  32580  elicc3  32632  bj-ssb1  32949  bj-snsetex  33261  bj-snglc  33267  bj-projun  33292  bj-vjust2  33325  wl-cases2-dnf  33611  poimirlem27  33749  mblfinlem2  33760  iscrngo2  34107  n0elqs  34413  inxpxrn  34466  prtlem70  34635  prtlem100  34638  prtlem15  34654  prter2  34660  lcvnbtwn3  34808  ishlat1  35132  ishlat2  35133  hlrelat2  35183  islpln5  35315  islvol5  35359  pclclN  35671  cdleme0nex  36071  aaitgo  38233  isdomn3  38283  imaiun1  38443  relexp0eq  38493  ntrk1k3eqk13  38848  2sbc6g  39115  2sbc5g  39116  2reu7  41703  2reu8  41704  alsconv  43107