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  1673  nfnbi  1855  2sb6  2087  2sb5  2278  dfsb7  2279  2sb5rf  2470  2sb6rf  2471  eu6lem  2566  eu6  2567  2mo2  2640  2eu7  2651  2eu8  2652  euae  2653  r2exlem  3122  r3al  3175  risset  3212  ralcom4  3263  rexcom4  3264  rabbi  3436  ralxpxfr2d  3612  reuind  3724  dfss2  3932  undif3  4263  unab  4271  inab  4272  n0el  4327  inssdif0  4337  ssundif  4451  raldifsnb  4760  pwtp  4866  uni0b  4897  iinuni  5062  inuni  5305  reusv2lem4  5356  pwtr  5412  opthprc  5702  xpiundir  5710  xpsspw  5772  relun  5774  inopab  5792  difopab  5793  difopabOLD  5794  ralxpf  5810  dmiun  5877  elidinxp  6015  iresn0n0  6025  inisegn0  6069  rniun  6120  imaco  6224  rnco  6225  mptfnf  6653  fnopabg  6655  dff1o2  6805  brprcneu  6848  brprcneuALT  6849  idref  7118  imaiun  7219  sorpss  7704  opabex3d  7944  opabex3rd  7945  opabex3  7946  ovmptss  8072  frpoins3xpg  8119  frpoins3xp3g  8120  poxp2  8122  poxp3  8129  fnsuppres  8170  sbthfilem  9162  ttrcltr  9669  rankc1  9823  aceq1  10070  dfac10  10091  fin41  10397  axgroth6  10781  genpass  10962  infm3  12142  prime  12615  elixx3g  13319  elfz2  13475  elfzuzb  13479  rpnnen2lem12  16193  divalgb  16374  1nprm  16649  maxprmfct  16679  vdwmc  16949  imasleval  17504  issubm  18730  issubg3  19076  efgrelexlemb  19680  isdomn5  20619  isdomn2  20620  isdomn3  20624  ist1-2  23234  unisngl  23414  elflim2  23851  isfcls  23896  istlm  24072  isnlm  24563  ishl2  25270  ovoliunlem1  25403  eln0s  28251  zaddscl  28282  readdscl  28350  remulscl  28353  erclwwlkref  29949  erclwwlknref  29998  0wlk  30045  h1de2ctlem  31484  nonbooli  31580  5oalem7  31589  ho01i  31757  rnbra  32036  cvnbtwn3  32217  chrelat2i  32294  difrab2  32427  uniinn0  32479  disjex  32521  maprnin  32654  ordtconnlem1  33914  esum2dlem  34082  eulerpartgbij  34363  eulerpartlemr  34365  eulerpartlemn  34372  ballotlem2  34480  bnj976  34767  bnj1185  34783  bnj543  34883  bnj571  34896  bnj611  34908  bnj916  34923  bnj1000  34931  bnj1040  34962  iscvm  35246  untuni  35696  dfso3  35707  dffr5  35741  elima4  35763  brtxpsd3  35884  brbigcup  35886  fixcnv  35896  ellimits  35898  elfuns  35903  brimage  35914  brcart  35920  brimg  35925  brapply  35926  brcup  35927  brcap  35928  dfrdg4  35939  dfint3  35940  ellines  36140  elicc3  36305  bj-snsetex  36951  bj-snglc  36957  bj-projun  36982  wl-2xor  37471  wl-cases2-dnf  37500  poimirlem27  37641  mblfinlem2  37652  iscrngo2  37991  n0elqs  38314  inxpxrn  38381  eqvrelcoss3  38609  prtlem70  38850  prtlem100  38852  prtlem15  38868  prter2  38874  lcvnbtwn3  39021  ishlat1  39345  ishlat2  39346  hlrelat2  39397  islpln5  39529  islvol5  39573  pclclN  39885  cdleme0nex  40284  eu6w  42664  aaitgo  43151  onmaxnelsup  43212  onsupnmax  43217  nnoeomeqom  43301  imaiun1  43640  relexp0eq  43690  ntrk1k3eqk13  44039  2sbc6g  44404  2sbc5g  44405  2reu7  47112  2reu8  47113  mosssn2  48805  iinxp  48819  ixpv  48878  alsconv  49779