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  818  pm4.78  934  xor  1016  cases2  1047  4anpull2  1362  nic-ax  1674  nfnbi  1856  2sb6  2089  2sb5  2280  dfsb7  2281  2sb5rf  2472  2sb6rf  2473  eu6lem  2568  eu6  2569  2mo2  2642  2eu7  2653  2eu8  2654  euae  2655  r2exlem  3121  r3al  3170  risset  3207  ralcom4  3258  rexcom4  3259  rabbi  3425  ralxpxfr2d  3601  reuind  3712  dfss2  3920  undif3  4250  unab  4258  inab  4259  n0el  4314  inssdif0  4324  ssundif  4438  raldifsnb  4748  pwtp  4854  uni0b  4885  iinuni  5046  inuni  5288  reusv2lem4  5339  pwtr  5393  opthprc  5680  xpiundir  5688  xpsspw  5749  relun  5751  inopab  5769  difopab  5770  ralxpf  5786  dmiun  5853  elidinxp  5993  iresn0n0  6003  inisegn0  6047  rniun  6094  imaco  6198  rnco  6199  rncoOLD  6200  mptfnf  6616  fnopabg  6618  dff1o2  6768  brprcneu  6812  brprcneuALT  6813  idref  7079  imaiun  7179  sorpss  7661  opabex3d  7897  opabex3rd  7898  opabex3  7899  ovmptss  8023  frpoins3xpg  8070  frpoins3xp3g  8071  poxp2  8073  poxp3  8080  fnsuppres  8121  sbthfilem  9107  ttrcltr  9606  rankc1  9763  aceq1  10008  dfac10  10029  fin41  10335  axgroth6  10719  genpass  10900  infm3  12081  prime  12554  elixx3g  13258  elfz2  13414  elfzuzb  13418  rpnnen2lem12  16134  divalgb  16315  1nprm  16590  maxprmfct  16620  vdwmc  16890  imasleval  17445  issubm  18711  issubg3  19057  efgrelexlemb  19663  isdomn5  20626  isdomn2  20627  isdomn3  20631  ist1-2  23263  unisngl  23443  elflim2  23880  isfcls  23925  istlm  24101  isnlm  24591  ishl2  25298  ovoliunlem1  25431  eln0s  28288  zaddscl  28319  readdscl  28402  remulscl  28405  erclwwlkref  29998  erclwwlknref  30047  0wlk  30094  h1de2ctlem  31533  nonbooli  31629  5oalem7  31638  ho01i  31806  rnbra  32085  cvnbtwn3  32266  chrelat2i  32343  difrab2  32475  uniinn0  32528  disjex  32570  maprnin  32712  ordtconnlem1  33935  esum2dlem  34103  eulerpartgbij  34383  eulerpartlemr  34385  eulerpartlemn  34392  ballotlem2  34500  bnj976  34787  bnj1185  34803  bnj543  34903  bnj571  34916  bnj611  34928  bnj916  34943  bnj1000  34951  bnj1040  34982  iscvm  35301  untuni  35751  dfso3  35762  dffr5  35796  elima4  35818  brtxpsd3  35936  brbigcup  35938  fixcnv  35948  ellimits  35950  elfuns  35955  brimage  35966  brcart  35972  brimg  35977  brapply  35978  brcup  35979  brcap  35980  dfrdg4  35991  dfint3  35992  ellines  36192  elicc3  36357  bj-snsetex  37003  bj-snglc  37009  bj-projun  37034  wl-2xor  37523  wl-cases2-dnf  37552  poimirlem27  37693  mblfinlem2  37704  iscrngo2  38043  n0elqs  38366  inxpxrn  38433  eqvrelcoss3  38661  prtlem70  38902  prtlem100  38904  prtlem15  38920  prter2  38926  lcvnbtwn3  39073  ishlat1  39397  ishlat2  39398  hlrelat2  39448  islpln5  39580  islvol5  39624  pclclN  39936  cdleme0nex  40335  eu6w  42715  aaitgo  43201  onmaxnelsup  43262  onsupnmax  43267  nnoeomeqom  43351  imaiun1  43690  relexp0eq  43740  ntrk1k3eqk13  44089  2sbc6g  44454  2sbc5g  44455  2reu7  47148  2reu8  47149  mosssn2  48854  iinxp  48868  ixpv  48927  alsconv  49828