ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4i Unicode version

Theorem 3bitr4i 201
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4i.1  |-  ( ph  <->  ps )
3bitr4i.2  |-  ( ch  <->  ph )
3bitr4i.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3bitr4i  |-  ( ch  <->  th )

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2  |-  ( ch  <->  ph )
2 3bitr4i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr4i.3 . . 3  |-  ( th  <->  ps )
42, 3bitr4i 176 . 2  |-  ( ph  <->  th )
51, 4bitri 173 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bibi2d  221  pm4.71  369  pm5.32ri  428  mpan10  443  an31  498  an4  520  or4  688  ordir  730  andir  732  dcbii  747  3anrot  890  3orrot  891  3ancoma  892  3orcomb  894  3ioran  900  3anbi123i  1093  3orbi123i  1094  3or6  1218  xorcom  1279  nfbii  1362  19.26-3an  1372  alnex  1388  19.42h  1577  19.42  1578  equsal  1615  sb6  1766  eeeanv  1808  sbbi  1833  sbco3xzyz  1847  sbcom2v  1861  sbel2x  1874  sb8eu  1913  sb8mo  1914  sb8euh  1923  eu1  1925  cbvmo  1940  mo3h  1953  sbmo  1959  eqcom  2042  abeq1  2147  cbvab  2160  clelab  2162  nfceqi  2174  sbabel  2203  ralbii2  2331  rexbii2  2332  r2alf  2338  r2exf  2339  nfraldya  2355  nfrexdya  2356  r3al  2363  r19.41  2462  r19.42v  2464  ralcomf  2468  rexcomf  2469  reean  2475  3reeanv  2477  rabid2  2483  rabbi  2484  reubiia  2491  rmobiia  2496  reu5  2519  rmo5  2522  cbvralf  2524  cbvrexf  2525  cbvreu  2528  cbvrmo  2529  vjust  2555  ceqsex3v  2593  ceqsex4v  2594  ceqsex8v  2596  eueq  2709  reu2  2726  reu6  2727  reu3  2728  rmo4  2731  2rmorex  2742  cbvsbc  2788  sbccomlem  2829  rmo3  2846  csbabg  2904  cbvralcsf  2905  cbvrexcsf  2906  cbvreucsf  2907  eqss  2957  uniiunlem  3025  ssequn1  3110  unss  3114  rexun  3120  ralunb  3121  elin3  3125  incom  3126  inass  3144  ssin  3156  nssinpss  3166  ssddif  3168  unssdif  3169  difin  3171  invdif  3176  indif  3177  indi  3181  symdifxor  3200  disj3  3269  rexsns  3406  reusn  3438  difsnpssim  3504  prss  3517  tpss  3526  eluni2  3581  elunirab  3590  uniun  3596  uni0b  3602  unissb  3607  elintrab  3624  ssintrab  3635  intun  3643  intpr  3644  iuncom  3660  iuncom4  3661  iunab  3700  ssiinf  3703  iinab  3715  iunin2  3717  iunun  3731  iunxun  3732  iunxiun  3733  sspwuni  3736  iinpw  3739  cbvdisj  3752  brun  3807  brin  3808  brdif  3809  dftr2  3853  inuni  3906  repizf2lem  3911  unidif0  3917  ssext  3954  pweqb  3956  otth2  3975  opelopabsbALT  3993  eqopab2b  4013  pwin  4016  unisuc  4146  sucexb  4219  elnn  4315  xpiundi  4385  xpiundir  4386  poinxp  4396  soinxp  4397  seinxp  4398  inopab  4455  difopab  4456  raliunxp  4464  rexiunxp  4465  iunxpf  4471  cnvco  4507  dmiun  4531  dmuni  4532  dm0rn0  4539  brres  4605  dmres  4619  cnvsym  4695  asymref  4697  codir  4700  qfto  4701  cnvopab  4713  cnvdif  4717  rniun  4721  dminss  4725  imainss  4726  cnvcnvsn  4784  resco  4812  imaco  4813  rnco  4814  coiun  4817  coass  4826  ressn  4845  cnviinm  4846  xpcom  4851  funcnv  4947  funcnv3  4948  fncnv  4952  fun11  4953  fnres  5002  dfmpt3  5008  fnopabg  5009  fintm  5062  fin  5063  fores  5102  dff1o3  5119  fun11iun  5134  f11o  5146  f1ompt  5307  fsn  5322  imaiun  5386  isores2  5440  eqoprab2b  5550  opabex3d  5735  opabex3  5736  dfopab2  5802  dfoprab3s  5803  fmpt2x  5813  tpostpos  5866  dfsmo2  5889  qsid  6158  xpassen  6291  diffitest  6330  distrnqg  6466  ltbtwnnq  6495  distrnq0  6538  nqprrnd  6622  ltresr  6896  elznn0nn  8231  xrnemnf  8666  xrnepnf  8667  elioomnf  8804  elxrge0  8814  elfzuzb  8851  fzass4  8892  elfz2nn0  8940  elfzo2  8974  elfzo3  8986  lbfzo0  9004  fzind2  9062  bdceq  9835
  Copyright terms: Public domain W3C validator