Theorem 3bitr4ri 304

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biadan  817  pm4.78  933  xor  1013  cases2  1046  nic-ax  1675  nfnbi  1857  2sb6  2089  2sb5  2272  dfsb7  2276  2sb5rf  2471  2sb6rf  2472  eu6lem  2572  eu6  2573  2mo2  2648  2eu7  2658  2eu8  2659  euae  2660  r2exlem  3137  r3al  3190  risset  3218  ralcom4  3266  rexcom4  3268  moelOLD  3375  ralxpxfr2d  3589  reuind  3703  undif3  4242  unab  4250  inab  4251  n0el  4313  inssdif0  4321  ab0  4326  ssundif  4437  ralf0OLD  4467  raldifsnb  4748  pwtp  4852  uniprOLD  4876  uni0b  4886  iinuni  5050  reusv2lem4  5349  pwtr  5402  opthprc  5687  xpiundir  5694  xpsspw  5756  relun  5758  inopab  5776  difopab  5777  difopabOLD  5778  ralxpf  5793  dmiun  5860  elidinxp  5988  iresn0n0  5998  inisegn0  6041  rniun  6091  imaco  6194  rnco  6195  mptfnf  6624  fnopabg  6626  dff1o2  6777  brprcneu  6820  brprcneuALT  6821  idref  7079  imaiun  7179  sorpss  7648  opabex3d  7881  opabex3rd  7882  opabex3  7883  ovmptss  8006  fnsuppres  8082  sbthfilem  9071  ttrcltr  9578  rankc1  9732  aceq1  9979  dfac10  9999  fin41  10306  axgroth6  10690  genpass  10871  infm3  12040  prime  12507  elixx3g  13198  elfz2  13352  elfzuzb  13356  rpnnen2lem12  16034  divalgb  16213  1nprm  16482  maxprmfct  16512  vdwmc  16777  imasleval  17350  issubm  18540  issubg3  18870  efgrelexlemb  19452  ist1-2  22604  unisngl  22784  elflim2  23221  isfcls  23266  istlm  23442  isnlm  23945  ishl2  24640  ovoliunlem1  24772  erclwwlkref  28672  erclwwlknref  28721  0wlk  28768  h1de2ctlem  30205  nonbooli  30301  5oalem7  30310  ho01i  30478  rnbra  30757  cvnbtwn3  30938  chrelat2i  31015  difrab2  31132  uniinn0  31175  disjex  31216  maprnin  31351  ordtconnlem1  32170  esum2dlem  32356  eulerpartgbij  32637  eulerpartlemr  32639  eulerpartlemn  32646  ballotlem2  32753  bnj976  33054  bnj1185  33070  bnj543  33170  bnj571  33183  bnj611  33195  bnj916  33210  bnj1000  33218  bnj1040  33249  iscvm  33518  untuni  33947  dfso3  33959  ralxp3f  33973  dffr5  34010  elima4  34033  frpoins3xpg  34069  frpoins3xp3g  34070  poxp2  34072  brtxpsd3  34335  brbigcup  34337  fixcnv  34347  ellimits  34349  elfuns  34354  brimage  34365  brcart  34371  brimg  34376  brapply  34377  brcup  34378  brcap  34379  dfrdg4  34390  dfint3  34391  ellines  34591  elicc3  34643  bj-snsetex  35288  bj-snglc  35294  bj-projun  35319  wl-2xor  35808  wl-cases2-dnf  35825  poimirlem27  35958  mblfinlem2  35969  iscrngo2  36309  n0elqs  36641  inxpxrn  36711  eqvrelcoss3  36934  prtlem70  37173  prtlem100  37175  prtlem15  37191  prter2  37197  lcvnbtwn3  37344  ishlat1  37668  ishlat2  37669  hlrelat2  37720  islpln5  37852  islvol5  37896  pclclN  38208  cdleme0nex  38607  isdomn5  40477  aaitgo  41299  isdomn3  41341  imaiun1  41630  relexp0eq  41680  ntrk1k3eqk13  42031  2sbc6g  42404  2sbc5g  42405  2reu7  45019  2reu8  45020  mosssn2  46578  iscnrm3lem3  46645  alsconv  46910