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  935  xor  1017  cases2  1048  4anpull2  1363  nic-ax  1675  nfnbi  1857  2sb6  2092  2sb5  2285  dfsb7  2286  2sb5rf  2477  2sb6rf  2478  eu6lem  2574  eu6  2575  2mo2  2648  2eu7  2659  2eu8  2660  euae  2661  r2exlem  3127  r3al  3176  risset  3213  ralcom4  3264  rexcom4  3265  rabbi  3420  ralxpxfr2d  3589  reuind  3700  dfss2  3908  undif3  4241  unab  4249  inab  4250  n0el  4305  inssdif0  4315  ssundif  4428  ralf0  4438  raldifsnb  4740  pwtp  4846  uni0b  4877  iinuni  5041  inuni  5287  reusv2lem4  5338  pwtr  5399  opthprc  5688  xpiundir  5696  xpsspw  5758  relun  5760  inopab  5778  difopab  5779  ralxpf  5795  dmiun  5862  elidinxp  6003  iresn0n0  6013  inisegn0  6057  rniun  6105  imaco  6209  rnco  6210  rncoOLD  6211  mptfnf  6627  fnopabg  6629  dff1o2  6779  brprcneu  6824  brprcneuALT  6825  idref  7093  imaiun  7193  sorpss  7675  opabex3d  7911  opabex3rd  7912  opabex3  7913  ovmptss  8036  frpoins3xpg  8083  frpoins3xp3g  8084  poxp2  8086  poxp3  8093  fnsuppres  8134  sbthfilem  9125  ttrcltr  9628  rankc1  9785  aceq1  10030  dfac10  10051  fin41  10357  axgroth6  10742  genpass  10923  infm3  12106  prime  12601  elixx3g  13302  elfz2  13459  elfzuzb  13463  rpnnen2lem12  16183  divalgb  16364  1nprm  16639  maxprmfct  16670  vdwmc  16940  imasleval  17496  issubm  18762  issubg3  19111  efgrelexlemb  19716  isdomn5  20678  isdomn2  20679  isdomn3  20683  ist1-2  23322  unisngl  23502  elflim2  23939  isfcls  23984  istlm  24160  isnlm  24650  ishl2  25347  ovoliunlem1  25479  eln0s  28367  zaddscl  28400  readdscl  28505  remulscl  28508  erclwwlkref  30105  erclwwlknref  30154  0wlk  30201  h1de2ctlem  31641  nonbooli  31737  5oalem7  31746  ho01i  31914  rnbra  32193  cvnbtwn3  32374  chrelat2i  32451  difrab2  32582  uniinn0  32635  disjex  32677  maprnin  32819  ordtconnlem1  34084  esum2dlem  34252  eulerpartgbij  34532  eulerpartlemr  34534  eulerpartlemn  34541  ballotlem2  34649  bnj976  34936  bnj1185  34951  bnj543  35051  bnj571  35064  bnj611  35076  bnj916  35091  bnj1000  35099  bnj1040  35130  iscvm  35457  untuni  35907  dfso3  35918  dffr5  35952  elima4  35974  brtxpsd3  36092  brbigcup  36094  fixcnv  36104  ellimits  36106  elfuns  36111  brimage  36122  brcart  36128  brimg  36133  brapply  36134  brcup  36135  brcap  36136  dfrdg4  36149  dfint3  36150  ellines  36350  elicc3  36515  bj-snsetex  37286  bj-snglc  37292  bj-projun  37317  wl-2xor  37813  wl-cases2-dnf  37851  poimirlem27  37982  mblfinlem2  37993  iscrngo2  38332  n0elqs  38667  inxpxrn  38753  eqvrelcoss3  39037  prtlem70  39317  prtlem100  39319  prtlem15  39335  prter2  39341  lcvnbtwn3  39488  ishlat1  39812  ishlat2  39813  hlrelat2  39863  islpln5  39995  islvol5  40039  pclclN  40351  cdleme0nex  40750  eu6w  43123  aaitgo  43608  onmaxnelsup  43669  onsupnmax  43674  nnoeomeqom  43758  imaiun1  44096  relexp0eq  44146  ntrk1k3eqk13  44495  2sbc6g  44860  2sbc5g  44861  2reu7  47571  2reu8  47572  mosssn2  49304  iinxp  49318  ixpv  49377  alsconv  50277