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  2316  dfsb7  2317  2sb5rf  2507  2sb6rf  2508  eu6lem  2604  eu6  2605  2mo2  2678  2eu7  2688  2eu8  2689  euae  2690  r2exlem  3157  r3al  3206  risset  3243  ralcom4  3294  rexcom4  3295  rabbi  3449  ralxpxfr2d  3608  reuind  3719  dfss2  3926  undif3  4256  unab  4264  inab  4265  n0el  4322  inssdif0OLD  4333  ssundif  4453  ralf0  4463  raldifsnb  4769  pwtp  4872  uni0b  4904  iinuni  5069  inuni  5325  reusv2lem4  5377  pwtr  5438  opthprc  5730  xpiundir  5738  xpsspw  5801  relun  5803  inopab  5821  difopab  5822  ralxpf  5837  dmiun  5908  elidinxp  6051  iresn0n0  6061  inisegn0  6105  rniun  6150  imaco  6257  rnco  6258  rncoOLD  6259  mptfnf  6677  fnopabg  6679  dff1o2  6833  brprcneu  6878  brprcneuALT  6879  idref  7149  imaiun  7250  sorpss  7738  opabex3d  7971  opabex3rd  7972  opabex3  7973  ovmptss  8097  frpoins3xpg  8145  frpoins3xp3g  8146  poxp2  8148  poxp3  8155  fnsuppres  8196  sbthfilem  9192  ttrcltr  9695  rankc1  9852  aceq1  10120  dfac10  10140  fin41  10446  axgroth6  10831  genpass  11012  infm3  12192  prime  12695  elixx3g  13403  elfz2  13560  elfzuzb  13564  rpnnen2lem12  16306  divalgb  16487  1nprm  16762  maxprmfct  16793  vdwmc  17063  imasleval  17620  issubm  18892  issubg3  19242  efgrelexlemb  19851  isdomn5  20846  isdomn2  20847  isdomn3  20850  ist1-2  23541  unisngl  23721  elflim2  24158  isfcls  24203  istlm  24379  isnlm  24869  ishl2  25566  ovoliunlem1  25698  eln0s  28591  zaddscl  28624  readdscl  28729  remulscl  28732  erclwwlkref  30408  erclwwlknref  30457  0wlk  30504  h1de2ctlem  31944  nonbooli  32040  5oalem7  32049  ho01i  32217  rnbra  32496  cvnbtwn3  32677  chrelat2i  32754  difrab2  32881  uniinn0  32934  disjex  32974  maprnin  33113  ordtconnlem1  34345  esum2dlem  34513  eulerpartgbij  34794  eulerpartlemr  34796  eulerpartlemn  34803  ballotlem2  34911  bnj976  35198  bnj1185  35213  bnj543  35313  bnj571  35326  bnj611  35338  bnj916  35353  bnj1000  35361  bnj1040  35392  iscvm  35772  untuni  36222  dfso3  36233  dffr5  36267  elima4  36289  brtxpsd3  36407  brbigcup  36409  fixcnv  36419  ellimits  36421  elfuns  36426  brimage  36437  brcart  36443  brimg  36448  brapply  36449  brcup  36450  brcap  36451  dfrdg4  36464  dfint3  36465  ellines  36665  elicc3  36869  bj-snsetex  37640  bj-snglc  37646  bj-projun  37671  wl-2xor  38170  wl-cases2-dnf  38208  poimirlem27  38339  mblfinlem2  38350  iscrngo2  38689  n0elqs  39022  inxpxrn  39108  eqvrelcoss3  39392  prtlem70  39672  prtlem100  39674  prtlem15  39690  prter2  39696  lcvnbtwn3  39843  ishlat1  40167  ishlat2  40168  hlrelat2  40218  islpln5  40350  islvol5  40394  pclclN  40706  cdleme0nex  41105  eu6w  43449  aaitgo  43930  onmaxnelsup  43991  onsupnmax  43996  nnoeomeqom  44080  imaiun1  44418  relexp0eq  44468  ntrk1k3eqk13  44817  2sbc6g  45166  2sbc5g  45167  2reu7  47889  2reu8  47890  mosssn2  49636  iinxp  49650  ixpv  49709