Theorem 3bitr4ri 307

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biadan  831  pm4.78  948  xor  1032  cases2  1063  4anpull2OLD  1383  nic-ax  1706  nfnbi  1888  2sb6  2123  2sb5  2312  dfsb7  2313  2sb5rf  2502  2sb6rf  2503  eu6lem  2599  eu6  2600  2mo2  2673  2eu7  2683  2eu8  2684  euae  2685  r2exlem  3152  r3al  3201  risset  3238  ralcom4  3289  rexcom4  3290  rabbi  3442  ralxpxfr2d  3600  reuind  3711  dfss2  3917  undif3  4246  unab  4254  inab  4255  n0el  4312  inssdif0OLD  4323  ssundif  4443  ralf0  4453  raldifsnb  4759  pwtp  4862  uni0b  4894  iinuni  5058  inuni  5311  reusv2lem4  5363  pwtr  5420  opthprc  5715  xpiundir  5723  xpsspw  5787  relun  5789  inopab  5807  difopab  5808  ralxpf  5824  dmiun  5895  elidinxp  6036  iresn0n0  6046  inisegn0  6096  rniun  6139  imaco  6251  rnco  6252  rncoOLD  6253  mptfnf  6672  fnopabg  6674  dff1o2  6828  brprcneu  6873  brprcneuALT  6874  idref  7147  imaiun  7247  sorpss  7742  opabex3d  7975  opabex3rd  7976  opabex3  7977  ovmptss  8102  frpoins3xpg  8150  frpoins3xp3g  8151  poxp2  8153  poxp3  8160  fnsuppres  8201  sbthfilem  9206  ttrcltr  9710  rankc1  9880  aceq1  10189  dfac10  10209  fin41  10515  axgroth6  10906  genpass  11087  infm3  12269  prime  12773  elixx3g  13482  elfz2  13639  elfzuzb  13643  rpnnen2lem12  16386  divalgb  16567  1nprm  16847  maxprmfct  16878  vdwmc  17149  imasleval  17706  issubm  18991  issubg3  19348  efgrelexlemb  19957  isdomn5  20955  isdomn2  20956  isdomn3  20959  ist1-2  23658  unisngl  23839  elflim2  24276  isfcls  24321  istlm  24497  isnlm  24987  ishl2  25684  ovoliunlem1  25816  eln0s  28740  zaddscl  28773  readdscl  28878  remulscl  28881  erclwwlkref  30604  erclwwlknref  30653  0wlk  30700  h1de2ctlem  32150  nonbooli  32246  5oalem7  32255  ho01i  32423  rnbra  32702  cvnbtwn3  32883  chrelat2i  32960  difrab2  33087  uniinn0  33140  disjex  33179  maprnin  33316  ordtconnlem1  34549  esum2dlem  34717  eulerpartgbij  34997  eulerpartlemr  34999  eulerpartlemn  35006  ballotlem2  35114  bnj976  35401  bnj1185  35416  bnj543  35516  bnj571  35529  bnj611  35541  bnj916  35556  bnj1000  35564  bnj1040  35595  iscvm  36003  untuni  36453  dfso3  36464  dffr5  36498  elima4  36520  brtxpsd3  36638  brbigcup  36640  fixcnv  36650  ellimits  36652  elfuns  36657  brimage  36668  brcart  36674  brimg  36679  brapply  36680  brcup  36681  brcap  36682  dfrdg4  36695  dfint3  36696  dffr7  36700  ellines  36897  elicc3  37085  bj-snsetex  37856  bj-snglc  37862  bj-projun  37887  wl-2xor  38386  wl-cases2-dnf  38424  poimirlem27  38545  mblfinlem2  38556  iscrngo2  38911  n0elqs  39244  inxpxrn  39330  eqvrelcoss3  39614  prtlem70  39894  prtlem100  39896  prtlem15  39912  prter2  39918  lcvnbtwn3  40065  ishlat1  40389  ishlat2  40390  hlrelat2  40440  islpln5  40572  islvol5  40616  pclclN  40928  cdleme0nex  41327  eu6w  43667  aaitgo  44148  onmaxnelsup  44209  onsupnmax  44214  nnoeomeqom  44298  imaiun1  44636  relexp0eq  44686  ntrk1k3eqk13  45035  2sbc6g  45384  2sbc5g  45385  2reu7  48150  2reu8  48151  mosssn2  49896  iinxp  49910  ixpv  49967