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  828  pm4.78  945  xor  1027  cases2  1058  4anpull2  1374  nic-ax  1692  nfnbi  1874  2sb6  2118  2sb5  2311  dfsb7  2312  2sb5rf  2502  2sb6rf  2503  eu6lem  2599  eu6  2600  2mo2  2673  2eu7  2683  2eu8  2684  euae  2685  r2exlem  3150  r3al  3199  risset  3236  ralcom4  3287  rexcom4  3288  rabbi  3443  ralxpxfr2d  3605  reuind  3715  dfss2  3922  undif3  4252  unab  4260  inab  4261  n0el  4316  inssdif0  4326  ssundif  4440  ralf0  4450  raldifsnb  4755  pwtp  4859  uni0b  4891  iinuni  5054  inuni  5305  reusv2lem4  5357  pwtr  5418  opthprc  5709  xpiundir  5717  xpsspw  5780  relun  5782  inopab  5800  difopab  5801  ralxpf  5816  dmiun  5887  elidinxp  6030  iresn0n0  6040  inisegn0  6084  rniun  6129  imaco  6234  rnco  6235  rncoOLD  6236  mptfnf  6652  fnopabg  6654  dff1o2  6808  brprcneu  6853  brprcneuALT  6854  idref  7124  imaiun  7225  sorpss  7707  opabex3d  7942  opabex3rd  7943  opabex3  7944  ovmptss  8067  frpoins3xpg  8115  frpoins3xp3g  8116  poxp2  8118  poxp3  8125  fnsuppres  8166  sbthfilem  9162  ttrcltr  9668  rankc1  9825  aceq1  10070  dfac10  10091  fin41  10398  axgroth6  10783  genpass  10964  infm3  12148  prime  12651  elixx3g  13359  elfz2  13516  elfzuzb  13520  rpnnen2lem12  16240  divalgb  16421  1nprm  16696  maxprmfct  16727  vdwmc  16997  imasleval  17554  issubm  18820  issubg3  19169  efgrelexlemb  19773  isdomn5  20739  isdomn2  20740  isdomn3  20744  ist1-2  23387  unisngl  23567  elflim2  24004  isfcls  24049  istlm  24225  isnlm  24715  ishl2  25412  ovoliunlem1  25544  eln0s  28431  zaddscl  28464  readdscl  28569  remulscl  28572  erclwwlkref  30168  erclwwlknref  30217  0wlk  30264  h1de2ctlem  31704  nonbooli  31800  5oalem7  31809  ho01i  31977  rnbra  32256  cvnbtwn3  32437  chrelat2i  32514  difrab2  32645  uniinn0  32699  disjex  32741  maprnin  32883  ordtconnlem1  34182  esum2dlem  34350  eulerpartgbij  34630  eulerpartlemr  34632  eulerpartlemn  34639  ballotlem2  34747  bnj976  35037  bnj1185  35052  bnj543  35152  bnj571  35165  bnj611  35177  bnj916  35192  bnj1000  35200  bnj1040  35231  iscvm  35573  untuni  36023  dfso3  36034  dffr5  36068  elima4  36090  brtxpsd3  36208  brbigcup  36210  fixcnv  36220  ellimits  36222  elfuns  36227  brimage  36238  brcart  36244  brimg  36249  brapply  36250  brcup  36251  brcap  36252  dfrdg4  36265  dfint3  36266  ellines  36466  elicc3  36641  bj-snsetex  37412  bj-snglc  37418  bj-projun  37443  wl-2xor  37941  wl-cases2-dnf  37979  poimirlem27  38110  mblfinlem2  38121  iscrngo2  38460  n0elqs  38795  inxpxrn  38881  eqvrelcoss3  39165  prtlem70  39445  prtlem100  39447  prtlem15  39463  prter2  39469  lcvnbtwn3  39616  ishlat1  39940  ishlat2  39941  hlrelat2  39991  islpln5  40123  islvol5  40167  pclclN  40479  cdleme0nex  40878  eu6w  43222  aaitgo  43703  onmaxnelsup  43764  onsupnmax  43769  nnoeomeqom  43853  imaiun1  44191  relexp0eq  44241  ntrk1k3eqk13  44590  2sbc6g  44955  2sbc5g  44956  2reu7  47669  2reu8  47670  mosssn2  49402  iinxp  49416  ixpv  49475  alsconv  50375