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

Theorem 3bitr4i 205
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 180 . 2  |-  ( ph  <->  th )
51, 4bitri 177 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bibi2d  225  pm4.71  375  pm5.32ri  436  mpan10  451  an31  506  an4  528  or4  698  ordir  741  andir  743  dcbii  758  3anrot  901  3orrot  902  3ancoma  903  3orcomb  905  3ioran  911  3anbi123i  1104  3orbi123i  1105  3or6  1229  xorcom  1295  nfbii  1378  19.26-3an  1388  alnex  1404  19.42h  1593  19.42  1594  equsal  1631  sb6  1782  eeeanv  1824  sbbi  1849  sbco3xzyz  1863  sbcom2v  1877  sbel2x  1890  sb8eu  1929  sb8mo  1930  sb8euh  1939  eu1  1941  cbvmo  1956  mo3h  1969  sbmo  1975  eqcom  2058  abeq1  2163  cbvab  2176  clelab  2178  nfceqi  2190  sbabel  2219  ralbii2  2351  rexbii2  2352  r2alf  2358  r2exf  2359  nfraldya  2375  nfrexdya  2376  r3al  2383  r19.41  2482  r19.42v  2484  ralcomf  2488  rexcomf  2489  reean  2495  3reeanv  2497  rabid2  2503  rabbi  2504  reubiia  2511  rmobiia  2516  reu5  2539  rmo5  2542  cbvralf  2544  cbvrexf  2545  cbvreu  2548  cbvrmo  2549  vjust  2575  ceqsex3v  2613  ceqsex4v  2614  ceqsex8v  2616  eueq  2735  reu2  2752  reu6  2753  reu3  2754  rmo4  2757  2rmorex  2768  cbvsbc  2814  sbccomlem  2860  rmo3  2877  csbabg  2935  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  eqss  2988  uniiunlem  3056  ssequn1  3141  unss  3145  rexun  3151  ralunb  3152  elin3  3156  incom  3157  inass  3175  ssin  3187  nssinpss  3197  ssddif  3199  unssdif  3200  difin  3202  invdif  3207  indif  3208  indi  3212  symdifxor  3231  disj3  3300  rexsns  3437  reusn  3469  difsnpssim  3535  prss  3548  tpss  3557  eluni2  3612  elunirab  3621  uniun  3627  uni0b  3633  unissb  3638  elintrab  3655  ssintrab  3666  intun  3674  intpr  3675  iuncom  3691  iuncom4  3692  iunab  3731  ssiinf  3734  iinab  3746  iunin2  3748  iunun  3762  iunxun  3763  iunxiun  3764  sspwuni  3767  iinpw  3770  cbvdisj  3783  brun  3838  brin  3839  brdif  3840  dftr2  3884  inuni  3937  repizf2lem  3942  unidif0  3948  ssext  3985  pweqb  3987  otth2  4006  opelopabsbALT  4024  eqopab2b  4044  pwin  4047  unisuc  4178  sucexb  4251  elnn  4356  xpiundi  4426  xpiundir  4427  poinxp  4437  soinxp  4438  seinxp  4439  inopab  4496  difopab  4497  raliunxp  4505  rexiunxp  4506  iunxpf  4512  cnvco  4548  dmiun  4572  dmuni  4573  dm0rn0  4580  brres  4646  dmres  4660  cnvsym  4736  asymref  4738  codir  4741  qfto  4742  cnvopab  4754  cnvdif  4758  rniun  4762  dminss  4766  imainss  4767  cnvcnvsn  4825  resco  4853  imaco  4854  rnco  4855  coiun  4858  coass  4867  ressn  4886  cnviinm  4887  xpcom  4892  funcnv  4988  funcnv3  4989  fncnv  4993  fun11  4994  fnres  5043  dfmpt3  5049  fnopabg  5050  fintm  5103  fin  5104  fores  5143  dff1o3  5160  fun11iun  5175  f11o  5187  f1ompt  5348  fsn  5363  imaiun  5427  isores2  5481  eqoprab2b  5591  opabex3d  5776  opabex3  5777  dfopab2  5843  dfoprab3s  5844  fmpt2x  5854  tpostpos  5910  dfsmo2  5933  qsid  6202  xpassen  6335  diffitest  6375  supmoti  6399  distrnqg  6543  ltbtwnnq  6572  distrnq0  6615  nqprrnd  6699  ltresr  6973  elznn0nn  8316  xrnemnf  8800  xrnepnf  8801  elioomnf  8938  elxrge0  8948  elfzuzb  8986  fzass4  9027  elfz2nn0  9075  elfzo2  9109  elfzo3  9121  lbfzo0  9139  fzind2  9197  rexfiuz  9816  bdceq  10349
  Copyright terms: Public domain W3C validator