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  1384  nic-ax  1706  nfnbi  1888  2sb6  2125  2sb5  2315  dfsb7  2316  2sb5rf  2504  2sb6rf  2505  eu6lem  2601  eu6  2602  2mo2  2675  2eu7  2685  2eu8  2686  euae  2687  r2exlem  3155  r3al  3204  risset  3241  ralcom4  3292  rexcom4  3293  rabbi  3445  ralxpxfr2d  3603  reuind  3714  dfss2  4097  undif3  4248  unab  4256  inab  4257  n0el  4315  inssdif0OLD  4326  ssundif  4446  ralf0  4456  raldifsnb  4759  pwtp  4832  uni0b  4897  iinuni  5061  inuni  5316  reusv2lem4  5368  pwtr  5425  opthprc  5720  xpiundir  5728  xpsspw  5794  relun  5796  inopab  5815  difopab  5816  ralxpf  5832  dmiun  5905  elidinxp  6052  iresn0n0  6062  inisegn0  6112  rniun  6155  imaco  6269  rnco  6270  rncoOLD  6271  mptfnf  6702  fnopabg  6704  dff1o2  6858  brprcneu  6904  brprcneuALT  6905  idref  7179  imaiun  7278  sorpss  7774  opabex3d  8009  opabex3rd  8010  opabex3  8011  ovmptssOLD  8138  frpoins3xpg  8192  frpoins3xp3g  8193  poxp2  8195  poxp3  8202  fnsuppres  8244  sbthfilem  9249  ttrcltr  9752  rankc1  9922  aceq1  10233  dfac10  10253  fin41  10559  axgroth6  10950  genpass  11131  infm3  12314  prime  12818  elixx3g  13527  elfz2  13684  elfzuzb  13688  rpnnen2lem12  16434  divalgb  16615  1nprm  16895  maxprmfct  16926  vdwmc  17197  imasleval  17754  issubm  19039  issubg3  19396  efgrelexlemb  20006  isdomn5  21004  isdomn2  21005  isdomn3  21008  ist1-2  23709  unisngl  23890  elflim2  24327  isfcls  24372  istlm  24548  isnlm  25038  ishl2  25735  ovoliunlem1  25867  eln0s  28793  zaddscl  28826  readdscl  28931  remulscl  28934  erclwwlkref  30657  erclwwlknref  30706  0wlk  30753  h1de2ctlem  32203  nonbooli  32299  5oalem7  32308  ho01i  32476  rnbra  32755  cvnbtwn3  32936  chrelat2i  33013  difrab2  33182  uniinn0  33235  disjex  33274  maprnin  33409  ordtconnlem1  34660  esum2dlem  34828  eulerpartgbij  35108  eulerpartlemr  35110  eulerpartlemn  35117  ballotlem2  35225  bnj976  35512  bnj1185  35527  bnj543  35627  bnj571  35640  bnj611  35652  bnj916  35667  bnj1000  35675  bnj1040  35706  rankse  35857  onprcf1acwevdlem1  36079  iscvm  36225  untuni  36682  dfso3  36693  dffr5  36727  elima4  36748  brtxpsd3  36866  brbigcup  36868  fixcnv  36878  ellimits  36880  elfuns  36885  brimage  36896  brcart  36902  brimg  36907  brapply  36908  brcup  36909  brcap  36910  dfrdg4  36923  dfint3  36924  dffr7  36928  ellines  37125  elicc3  37313  bj-snsetex  38084  bj-snglc  38090  bj-projun  38115  bj-inxpALT  38169  wl-2xor  38667  wl-cases2-dnf  38705  poimirlem27  38826  mblfinlem2  38837  iscrngo2  39190  n0elqs  39523  inxpxrn  39609  eqvrelcoss3  39893  prtlem70  40173  prtlem100  40175  prtlem15  40191  prter2  40197  lcvnbtwn3  40344  ishlat1  40668  ishlat2  40669  hlrelat2  40719  islpln5  40851  islvol5  40895  pclclN  41207  cdleme0nex  41606  eu6w  43947  aaitgo  44423  onmaxnelsup  44480  onsupnmax  44485  nnoeomeqom  44569  imaiun1  44906  relexp0eq  44956  ntrk1k3eqk13  45305  2sbc6g  45654  2sbc5g  45655  2reu7  48449  2reu8  48450  rrx2xpref1o  50156  mosssn2  50253  iinxp  50267  ixpv  50328