Theorem 3bitr4ri 293

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  pm4.78  605  xor  953  cases2  1016  nannan  1491  nic-ax  1638  2sb5  2471  2sb6  2472  2sb5rf  2479  moabs  2530  2mo2  2579  2eu7  2588  2eu8  2589  r3al  2969  r2exlem  3088  risset  3091  r19.35  3113  ralxpxfr2d  3358  reuind  3444  undif3  3921  undif3OLD  3922  unab  3927  inab  3928  n0el  3973  inssdif0  3980  ssundif  4085  ralf0  4111  raldifsnb  4358  pwtp  4463  unipr  4481  uni0b  4495  iinuni  4641  reusv2lem4  4902  pwtr  4951  elxp2OLD  5167  opthprc  5201  xpiundir  5208  xpsspw  5266  relun  5268  inopab  5285  difopab  5286  ralxpf  5301  dmiun  5365  inisegn0  5532  rniun  5578  imaco  5678  mptfnf  6053  fnopabg  6055  dff1o2  6180  brprcneu  6222  idref  6539  imaiun  6543  sorpss  6984  opabex3d  7187  opabex3  7188  ovmptss  7303  fnsuppres  7367  rankc1  8771  aceq1  8978  dfac10  8997  fin41  9304  axgroth6  9688  genpass  9869  infm3  11020  prime  11496  elixx3g  12226  elfz2  12371  elfzuzb  12374  rpnnen2lem12  14998  divalgb  15174  1nprm  15439  maxprmfct  15468  vdwmc  15729  imasleval  16248  issubm  17394  issubg3  17659  efgrelexlemb  18209  ist1-2  21199  unisngl  21378  elflim2  21815  isfcls  21860  istlm  22035  isnlm  22526  ishl2  23212  erclwwlkref  26977  erclwwlknref  27033  0wlk  27094  h1de2ctlem  28542  nonbooli  28638  5oalem7  28647  ho01i  28815  rnbra  29094  cvnbtwn3  29275  chrelat2i  29352  moel  29451  difrab2  29465  uniinn0  29492  disjex  29531  maprnin  29634  ordtconnlem1  30098  esum2dlem  30282  eulerpartgbij  30562  eulerpartlemr  30564  eulerpartlemn  30571  ballotlem2  30678  bnj976  30974  bnj1185  30990  bnj543  31089  bnj571  31102  bnj611  31114  bnj916  31129  bnj1000  31137  bnj1040  31166  iscvm  31367  untuni  31712  dfso3  31727  dffr5  31769  elima4  31803  brtxpsd3  32128  brbigcup  32130  fixcnv  32140  ellimits  32142  elfuns  32147  brimage  32158  brcart  32164  brimg  32169  brapply  32170  brcup  32171  brcap  32172  dfrdg4  32183  dfint3  32184  ellines  32384  elicc3  32436  bj-ssb1  32758  bj-snsetex  33076  bj-snglc  33082  bj-projun  33107  bj-vjust2  33140  wl-cases2-dnf  33425  poimirlem27  33566  mblfinlem2  33577  iscrngo2  33926  ralanid  34152  n0elqs  34239  inxpxrn  34293  prtlem70  34460  prtlem100  34463  prtlem15  34479  prter2  34485  lcvnbtwn3  34633  ishlat1  34957  ishlat2  34958  hlrelat2  35007  islpln5  35139  islvol5  35183  pclclN  35495  cdleme0nex  35895  aaitgo  38049  isdomn3  38099  imaiun1  38260  relexp0eq  38310  ntrk1k3eqk13  38665  2sbc6g  38933  2sbc5g  38934  2reu7  41512  2reu8  41513  alsconv  42864