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 206

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 207

This theorem is referenced by:  biadan  819  pm4.78  934  xor  1016  cases2  1047  nic-ax  1669  nfnbi  1851  2sb6  2083  2sb5  2275  dfsb7  2277  2sb5rf  2474  2sb6rf  2475  eu6lem  2570  eu6  2571  2mo2  2644  2eu7  2655  2eu8  2656  euae  2657  r2exlem  3140  r3al  3194  risset  3230  ralcom4  3283  rexcom4  3285  moelOLD  3402  rabbi  3464  ralxpxfr2d  3645  reuind  3761  dfss2  3980  undif3  4305  unab  4313  inab  4314  n0el  4369  inssdif0  4379  ssundif  4493  raldifsnb  4800  pwtp  4906  uni0b  4937  iinuni  5102  inuni  5355  reusv2lem4  5406  pwtr  5462  opthprc  5752  xpiundir  5759  xpsspw  5821  relun  5823  inopab  5841  difopab  5842  difopabOLD  5843  ralxpf  5859  dmiun  5926  elidinxp  6063  iresn0n0  6073  inisegn0  6118  rniun  6169  imaco  6272  rnco  6273  mptfnf  6703  fnopabg  6705  dff1o2  6853  brprcneu  6896  brprcneuALT  6897  idref  7165  imaiun  7264  sorpss  7746  opabex3d  7988  opabex3rd  7989  opabex3  7990  ovmptss  8116  frpoins3xpg  8163  frpoins3xp3g  8164  poxp2  8166  poxp3  8173  fnsuppres  8214  sbthfilem  9235  ttrcltr  9753  rankc1  9907  aceq1  10154  dfac10  10175  fin41  10481  axgroth6  10865  genpass  11046  infm3  12224  prime  12696  elixx3g  13396  elfz2  13550  elfzuzb  13554  rpnnen2lem12  16257  divalgb  16437  1nprm  16712  maxprmfct  16742  vdwmc  17011  imasleval  17587  issubm  18828  issubg3  19174  efgrelexlemb  19782  isdomn5  20726  isdomn2  20727  isdomn3  20731  ist1-2  23370  unisngl  23550  elflim2  23987  isfcls  24032  istlm  24208  isnlm  24711  ishl2  25417  ovoliunlem1  25550  eln0s  28372  zaddscl  28394  readdscl  28445  remulscl  28448  erclwwlkref  30048  erclwwlknref  30097  0wlk  30144  h1de2ctlem  31583  nonbooli  31679  5oalem7  31688  ho01i  31856  rnbra  32135  cvnbtwn3  32316  chrelat2i  32393  difrab2  32525  uniinn0  32570  disjex  32611  maprnin  32748  ordtconnlem1  33884  esum2dlem  34072  eulerpartgbij  34353  eulerpartlemr  34355  eulerpartlemn  34362  ballotlem2  34469  bnj976  34769  bnj1185  34785  bnj543  34885  bnj571  34898  bnj611  34910  bnj916  34925  bnj1000  34933  bnj1040  34964  iscvm  35243  untuni  35688  dfso3  35699  dffr5  35733  elima4  35756  brtxpsd3  35877  brbigcup  35879  fixcnv  35889  ellimits  35891  elfuns  35896  brimage  35907  brcart  35913  brimg  35918  brapply  35919  brcup  35920  brcap  35921  dfrdg4  35932  dfint3  35933  ellines  36133  elicc3  36299  bj-snsetex  36945  bj-snglc  36951  bj-projun  36976  wl-2xor  37465  wl-cases2-dnf  37492  poimirlem27  37633  mblfinlem2  37644  iscrngo2  37983  n0elqs  38307  inxpxrn  38376  eqvrelcoss3  38599  prtlem70  38838  prtlem100  38840  prtlem15  38856  prter2  38862  lcvnbtwn3  39009  ishlat1  39333  ishlat2  39334  hlrelat2  39385  islpln5  39517  islvol5  39561  pclclN  39873  cdleme0nex  40272  eu6w  42662  aaitgo  43150  onmaxnelsup  43211  onsupnmax  43216  nnoeomeqom  43301  imaiun1  43640  relexp0eq  43690  ntrk1k3eqk13  44039  2sbc6g  44410  2sbc5g  44411  2reu7  47060  2reu8  47061  mosssn2  48664  iscnrm3lem3  48731  alsconv  49020