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

Theorem 3bitr4i 211
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 186 . 2  |-  ( ph  <->  th )
51, 4bitri 183 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bibi2d  231  pm4.71  386  pm5.32ri  450  mpan10  465  an31  538  an4  560  or4  745  ordir  791  andir  793  3anrot  952  3orrot  953  3ancoma  954  3orcomb  956  3ioran  962  3anbi123i  1155  3orbi123i  1156  3or6  1286  xorcom  1351  nfbii  1434  19.26-3an  1444  alnex  1460  19.42h  1650  19.42  1651  equsal  1690  sb6  1842  eeeanv  1885  sbbi  1910  sbco3xzyz  1924  sbcom2v  1938  sbel2x  1951  sb8eu  1990  sb8mo  1991  sb8euh  2000  eu1  2002  cbvmo  2017  mo3h  2030  sbmo  2036  eqcom  2119  abeq1  2227  cbvab  2240  clelab  2242  nfceqi  2254  sbabel  2284  ralbii2  2422  rexbii2  2423  r2alf  2429  r2exf  2430  nfraldya  2446  nfrexdya  2447  r3al  2454  r19.41  2563  r19.42v  2565  ralcomf  2569  rexcomf  2570  reean  2576  3reeanv  2578  rabid2  2584  rabbi  2585  reubiia  2592  rmobiia  2597  reu5  2620  rmo5  2623  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvrmo  2630  vjust  2661  ceqsex3v  2702  ceqsex4v  2703  ceqsex8v  2705  eueq  2828  reu2  2845  reu6  2846  reu3  2847  rmo4  2850  rmo3f  2854  2rmorex  2863  cbvsbc  2909  sbccomlem  2955  rmo3  2972  csbabg  3031  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  eqss  3082  uniiunlem  3155  ssequn1  3216  unss  3220  rexun  3226  ralunb  3227  elin3  3237  incom  3238  inass  3256  ssin  3268  ssddif  3280  unssdif  3281  difin  3283  invdif  3288  indif  3289  indi  3293  symdifxor  3312  disj3  3385  rexsns  3533  reusn  3564  prss  3646  tpss  3655  eluni2  3710  elunirab  3719  uniun  3725  uni0b  3731  unissb  3736  elintrab  3753  ssintrab  3764  intun  3772  intpr  3773  iuncom  3789  iuncom4  3790  iunab  3829  ssiinf  3832  iinab  3844  iunin2  3846  iunun  3861  iunxun  3862  iunxiun  3864  sspwuni  3867  iinpw  3873  cbvdisj  3886  brun  3949  brin  3950  brdif  3951  dftr2  3998  inuni  4050  repizf2lem  4055  unidif0  4061  ssext  4113  pweqb  4115  otth2  4133  opelopabsbALT  4151  eqopab2b  4171  pwin  4174  unisuc  4305  elpwpwel  4366  sucexb  4383  elnn  4489  xpiundi  4567  xpiundir  4568  poinxp  4578  soinxp  4579  seinxp  4580  inopab  4641  difopab  4642  raliunxp  4650  rexiunxp  4651  iunxpf  4657  cnvco  4694  dmiun  4718  dmuni  4719  dm0rn0  4726  brres  4795  dmres  4810  cnvsym  4892  asymref  4894  codir  4897  qfto  4898  cnvopab  4910  cnvdif  4915  rniun  4919  dminss  4923  imainss  4924  cnvcnvsn  4985  resco  5013  imaco  5014  rnco  5015  coiun  5018  coass  5027  ressn  5049  cnviinm  5050  xpcom  5055  funcnv  5154  funcnv3  5155  fncnv  5159  fun11  5160  fnres  5209  dfmpt3  5215  fnopabg  5216  fintm  5278  fin  5279  fores  5324  dff1o3  5341  fun11iun  5356  f11o  5368  f1ompt  5539  fsn  5560  imaiun  5629  isores2  5682  eqoprab2b  5797  opabex3d  5987  opabex3  5988  dfopab2  6055  dfoprab3s  6056  fmpox  6066  tpostpos  6129  dfsmo2  6152  qsid  6462  mapval2  6540  mapsncnv  6557  elixp2  6564  ixpin  6585  xpassen  6692  diffitest  6749  supmoti  6848  eqinfti  6875  distrnqg  7163  ltbtwnnq  7192  distrnq0  7235  nqprrnd  7319  ltresr  7615  elznn0nn  9026  xrnemnf  9519  xrnepnf  9520  elioomnf  9706  elxrge0  9716  elfzuzb  9755  fzass4  9797  elfz2nn0  9847  elfzo2  9882  elfzo3  9895  lbfzo0  9913  fzind2  9971  rexfiuz  10716  fisumcom2  11162  infssuzex  11554  isbasis2g  12123  tgval2  12131  ntreq0  12212  txuni2  12336  isms2  12534  bdceq  12936
  Copyright terms: Public domain W3C validator