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  1383  nic-ax  1706  nfnbi  1888  2sb6  2123  2sb5  2313  dfsb7  2314  2sb5rf  2503  2sb6rf  2504  eu6lem  2600  eu6  2601  2mo2  2674  2eu7  2684  2eu8  2685  euae  2686  r2exlem  3153  r3al  3202  risset  3239  ralcom4  3290  rexcom4  3291  rabbi  3444  ralxpxfr2d  3603  reuind  3714  dfss2  3920  undif3  4249  unab  4257  inab  4258  n0el  4315  inssdif0OLD  4326  ssundif  4446  ralf0  4456  raldifsnb  4762  pwtp  4865  uni0b  4897  iinuni  5062  inuni  5318  reusv2lem4  5370  pwtr  5431  opthprc  5723  xpiundir  5731  xpsspw  5794  relun  5796  inopab  5814  difopab  5815  ralxpf  5830  dmiun  5901  elidinxp  6044  iresn0n0  6054  inisegn0  6098  rniun  6143  imaco  6251  rnco  6252  rncoOLD  6253  mptfnf  6671  fnopabg  6673  dff1o2  6827  brprcneu  6872  brprcneuALT  6873  idref  7146  imaiun  7246  sorpss  7733  opabex3d  7966  opabex3rd  7967  opabex3  7968  ovmptss  8094  frpoins3xpg  8142  frpoins3xp3g  8143  poxp2  8145  poxp3  8152  fnsuppres  8193  sbthfilem  9196  ttrcltr  9699  rankc1  9856  aceq1  10124  dfac10  10144  fin41  10450  axgroth6  10841  genpass  11022  infm3  12202  prime  12706  elixx3g  13415  elfz2  13572  elfzuzb  13576  rpnnen2lem12  16319  divalgb  16500  1nprm  16775  maxprmfct  16806  vdwmc  17076  imasleval  17633  issubm  18917  issubg3  19274  efgrelexlemb  19883  isdomn5  20878  isdomn2  20879  isdomn3  20882  ist1-2  23578  unisngl  23759  elflim2  24196  isfcls  24241  istlm  24417  isnlm  24907  ishl2  25604  ovoliunlem1  25736  eln0s  28634  zaddscl  28667  readdscl  28772  remulscl  28775  erclwwlkref  30498  erclwwlknref  30547  0wlk  30594  h1de2ctlem  32044  nonbooli  32140  5oalem7  32149  ho01i  32317  rnbra  32596  cvnbtwn3  32777  chrelat2i  32854  difrab2  32981  uniinn0  33034  disjex  33073  maprnin  33210  ordtconnlem1  34442  esum2dlem  34610  eulerpartgbij  34891  eulerpartlemr  34893  eulerpartlemn  34900  ballotlem2  35008  bnj976  35295  bnj1185  35310  bnj543  35410  bnj571  35423  bnj611  35435  bnj916  35450  bnj1000  35458  bnj1040  35489  iscvm  35846  untuni  36296  dfso3  36307  dffr5  36341  elima4  36363  brtxpsd3  36481  brbigcup  36483  fixcnv  36493  ellimits  36495  elfuns  36500  brimage  36511  brcart  36517  brimg  36522  brapply  36523  brcup  36524  brcap  36525  dfrdg4  36538  dfint3  36539  dffr7  36543  ellines  36740  elicc3  36944  bj-snsetex  37715  bj-snglc  37721  bj-projun  37746  wl-2xor  38245  wl-cases2-dnf  38283  poimirlem27  38404  mblfinlem2  38415  iscrngo2  38755  n0elqs  39088  inxpxrn  39174  eqvrelcoss3  39458  prtlem70  39738  prtlem100  39740  prtlem15  39756  prter2  39762  lcvnbtwn3  39909  ishlat1  40233  ishlat2  40234  hlrelat2  40284  islpln5  40416  islvol5  40460  pclclN  40772  cdleme0nex  41171  eu6w  43530  aaitgo  44011  onmaxnelsup  44072  onsupnmax  44077  nnoeomeqom  44161  imaiun1  44499  relexp0eq  44549  ntrk1k3eqk13  44898  2sbc6g  45247  2sbc5g  45248  2reu7  48007  2reu8  48008  mosssn2  49753  iinxp  49767  ixpv  49824