Theorem 3bitr4ri 296

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  biadan  807  pm4.78  919  xor  998  cases2  1029  nannanOLD  1472  nic-ax  1637  2sb5  2211  2sb6  2212  dfsb7  2213  2sb5rf  2419  2sb6rf  2420  eu6lem  2590  eu6  2591  moabsOLD  2631  2mo2  2680  2eu7  2691  2eu8  2692  euae  2693  ralanidOLD  3114  r3al  3147  risset  3208  r2exlem  3242  ralxpxfr2d  3549  reuind  3648  undif3  4147  unab  4152  inab  4153  n0el  4202  inssdif0  4210  ssundif  4311  ralf0  4335  raldifsnb  4600  pwtp  4704  unipr  4722  uni0b  4734  iinuni  4883  reusv2lem4  5152  pwtr  5199  opthprc  5463  xpiundir  5470  xpsspw  5529  relun  5531  inopab  5548  difopab  5549  ralxpf  5564  dmiun  5629  elidinxp  5754  inisegn0  5799  rniun  5844  imaco  5941  rnco  5942  mptfnf  6311  fnopabg  6313  dff1o2  6447  brprcneu  6489  idref  6730  imaiun  6828  sorpss  7271  opabex3d  7477  opabex3rd  7478  opabex3  7479  ovmptss  7595  fnsuppres  7659  rankc1  9092  aceq1  9336  dfac10  9356  fin41  9663  axgroth6  10047  genpass  10228  infm3  11400  prime  11875  elixx3g  12566  elfz2  12714  elfzuzb  12717  rpnnen2lem12  15437  divalgb  15614  1nprm  15878  maxprmfct  15908  vdwmc  16169  imasleval  16669  issubm  17828  issubg3  18094  efgrelexlemb  18649  ist1-2  21675  unisngl  21855  elflim2  22292  isfcls  22337  istlm  22512  isnlm  23003  ishl2  23692  ovoliunlem1  23822  erclwwlkref  27551  erclwwlknref  27609  0wlk  27661  h1de2ctlem  29129  nonbooli  29225  5oalem7  29234  ho01i  29402  rnbra  29681  cvnbtwn3  29862  chrelat2i  29939  moel  30050  difrab2  30056  uniinn0  30088  disjex  30126  maprnin  30244  ordtconnlem1  30844  esum2dlem  31028  eulerpartgbij  31308  eulerpartlemr  31310  eulerpartlemn  31317  ballotlem2  31425  bnj976  31730  bnj1185  31746  bnj543  31845  bnj571  31858  bnj611  31870  bnj916  31885  bnj1000  31893  bnj1040  31922  iscvm  32124  untuni  32488  dfso3  32503  dffr5  32542  elima4  32572  brtxpsd3  32911  brbigcup  32913  fixcnv  32923  ellimits  32925  elfuns  32930  brimage  32941  brcart  32947  brimg  32952  brapply  32953  brcup  32954  brcap  32955  dfrdg4  32966  dfint3  32967  ellines  33167  elicc3  33219  bj-snsetex  33826  bj-snglc  33832  bj-projun  33857  bj-vjust  33890  wl-cases2-dnf  34226  poimirlem27  34393  mblfinlem2  34404  iscrngo2  34750  n0elqs  35061  inxpxrn  35121  eqvrelcoss3  35331  prtlem70  35471  prtlem100  35473  prtlem15  35489  prter2  35495  lcvnbtwn3  35642  ishlat1  35966  ishlat2  35967  hlrelat2  36017  islpln5  36149  islvol5  36193  pclclN  36505  cdleme0nex  36904  aaitgo  39192  isdomn3  39234  imaiun1  39393  relexp0eq  39443  ntrk1k3eqk13  39797  2sbc6g  40198  2sbc5g  40199  2reu7  42746  2reu8  42747  alsconv  44288