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 205

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 206

This theorem is referenced by:  biadan  818  pm4.78  934  xor  1014  cases2  1047  nic-ax  1676  nfnbi  1858  2sb6  2090  2sb5  2272  dfsb7  2276  2sb5rf  2472  2sb6rf  2473  eu6lem  2568  eu6  2569  2mo2  2644  2eu7  2654  2eu8  2655  euae  2656  r2exlem  3144  r3al  3197  risset  3231  ralcom4  3284  rexcom4  3286  moelOLD  3402  rabbi  3463  ralxpxfr2d  3634  reuind  3749  undif3  4290  unab  4298  inab  4299  n0el  4361  inssdif0  4369  ssundif  4487  ralf0OLD  4517  raldifsnb  4799  pwtp  4903  uniprOLD  4927  uni0b  4937  iinuni  5101  reusv2lem4  5399  pwtr  5452  opthprc  5739  xpiundir  5746  xpsspw  5808  relun  5810  inopab  5828  difopab  5829  difopabOLD  5830  ralxpf  5845  dmiun  5912  elidinxp  6042  iresn0n0  6052  inisegn0  6095  rniun  6145  imaco  6248  rnco  6249  mptfnf  6683  fnopabg  6685  dff1o2  6836  brprcneu  6879  brprcneuALT  6880  idref  7141  imaiun  7241  sorpss  7715  opabex3d  7949  opabex3rd  7950  opabex3  7951  ovmptss  8076  frpoins3xpg  8123  frpoins3xp3g  8124  poxp2  8126  poxp3  8133  fnsuppres  8173  sbthfilem  9198  ttrcltr  9708  rankc1  9862  aceq1  10109  dfac10  10129  fin41  10436  axgroth6  10820  genpass  11001  infm3  12170  prime  12640  elixx3g  13334  elfz2  13488  elfzuzb  13492  rpnnen2lem12  16165  divalgb  16344  1nprm  16613  maxprmfct  16643  vdwmc  16908  imasleval  17484  issubm  18681  issubg3  19019  efgrelexlemb  19613  isdomn5  20910  ist1-2  22843  unisngl  23023  elflim2  23460  isfcls  23505  istlm  23681  isnlm  24184  ishl2  24879  ovoliunlem1  25011  erclwwlkref  29263  erclwwlknref  29312  0wlk  29359  h1de2ctlem  30796  nonbooli  30892  5oalem7  30901  ho01i  31069  rnbra  31348  cvnbtwn3  31529  chrelat2i  31606  difrab2  31726  uniinn0  31770  disjex  31811  maprnin  31944  ordtconnlem1  32893  esum2dlem  33079  eulerpartgbij  33360  eulerpartlemr  33362  eulerpartlemn  33369  ballotlem2  33476  bnj976  33777  bnj1185  33793  bnj543  33893  bnj571  33906  bnj611  33918  bnj916  33933  bnj1000  33941  bnj1040  33972  iscvm  34239  untuni  34667  dfso3  34678  dffr5  34713  elima4  34736  brtxpsd3  34857  brbigcup  34859  fixcnv  34869  ellimits  34871  elfuns  34876  brimage  34887  brcart  34893  brimg  34898  brapply  34899  brcup  34900  brcap  34901  dfrdg4  34912  dfint3  34913  ellines  35113  elicc3  35191  bj-snsetex  35833  bj-snglc  35839  bj-projun  35864  wl-2xor  36353  wl-cases2-dnf  36370  poimirlem27  36504  mblfinlem2  36515  iscrngo2  36854  n0elqs  37184  inxpxrn  37254  eqvrelcoss3  37477  prtlem70  37716  prtlem100  37718  prtlem15  37734  prter2  37740  lcvnbtwn3  37887  ishlat1  38211  ishlat2  38212  hlrelat2  38263  islpln5  38395  islvol5  38439  pclclN  38751  cdleme0nex  39150  aaitgo  41890  isdomn3  41932  onmaxnelsup  41958  onsupnmax  41963  nnoeomeqom  42048  imaiun1  42388  relexp0eq  42438  ntrk1k3eqk13  42787  2sbc6g  43160  2sbc5g  43161  2reu7  45806  2reu8  45807  mosssn2  47455  iscnrm3lem3  47522  alsconv  47791