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  553  an4  575  or4  760  ordir  806  andir  808  3anrot  967  3orrot  968  3ancoma  969  3orcomb  971  3ioran  977  3anbi123i  1170  3orbi123i  1171  3or6  1301  xorcom  1366  nfbii  1449  19.26-3an  1459  alnex  1475  19.42h  1665  19.42  1666  equsal  1705  sb6  1858  eeeanv  1905  sbbi  1932  sbco3xzyz  1946  sbcom2v  1960  sbel2x  1973  sb8eu  2012  sb8mo  2013  sb8euh  2022  eu1  2024  cbvmo  2039  mo3h  2052  sbmo  2058  eqcom  2141  abeq1  2249  cbvabw  2262  cbvab  2263  clelab  2265  nfceqi  2277  sbabel  2307  ralbii2  2445  rexbii2  2446  r2alf  2452  r2exf  2453  nfraldya  2469  nfrexdya  2470  r3al  2477  r19.41  2586  r19.42v  2588  ralcomf  2592  rexcomf  2593  reean  2599  3reeanv  2601  rabid2  2607  rabbi  2608  reubiia  2615  rmobiia  2620  reu5  2643  rmo5  2646  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvrmo  2653  vjust  2687  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  eueq  2855  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  rmo3f  2881  2rmorex  2890  cbvsbcw  2936  cbvsbc  2937  sbccomlem  2983  rmo3  3000  csbabg  3061  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  eqss  3112  uniiunlem  3185  ssequn1  3246  unss  3250  rexun  3256  ralunb  3257  elin3  3267  incom  3268  inass  3286  ssin  3298  ssddif  3310  unssdif  3311  difin  3313  invdif  3318  indif  3319  indi  3323  symdifxor  3342  disj3  3415  rexsns  3563  reusn  3594  prss  3676  tpss  3685  eluni2  3740  elunirab  3749  uniun  3755  uni0b  3761  unissb  3766  elintrab  3783  ssintrab  3794  intun  3802  intpr  3803  iuncom  3819  iuncom4  3820  iunab  3859  ssiinf  3862  iinab  3874  iunin2  3876  iunun  3891  iunxun  3892  iunxiun  3894  sspwuni  3897  iinpw  3903  cbvdisj  3916  brun  3979  brin  3980  brdif  3981  dftr2  4028  inuni  4080  repizf2lem  4085  unidif0  4091  ssext  4143  pweqb  4145  otth2  4163  opelopabsbALT  4181  eqopab2b  4201  pwin  4204  unisuc  4335  elpwpwel  4396  sucexb  4413  elnn  4519  xpiundi  4597  xpiundir  4598  poinxp  4608  soinxp  4609  seinxp  4610  inopab  4671  difopab  4672  raliunxp  4680  rexiunxp  4681  iunxpf  4687  cnvco  4724  dmiun  4748  dmuni  4749  dm0rn0  4756  brres  4825  dmres  4840  cnvsym  4922  asymref  4924  codir  4927  qfto  4928  cnvopab  4940  cnvdif  4945  rniun  4949  dminss  4953  imainss  4954  cnvcnvsn  5015  resco  5043  imaco  5044  rnco  5045  coiun  5048  coass  5057  ressn  5079  cnviinm  5080  xpcom  5085  funcnv  5184  funcnv3  5185  fncnv  5189  fun11  5190  fnres  5239  dfmpt3  5245  fnopabg  5246  fintm  5308  fin  5309  fores  5354  dff1o3  5373  fun11iun  5388  f11o  5400  f1ompt  5571  fsn  5592  imaiun  5661  isores2  5714  eqoprab2b  5829  opabex3d  6019  opabex3  6020  dfopab2  6087  dfoprab3s  6088  fmpox  6098  tpostpos  6161  dfsmo2  6184  qsid  6494  mapval2  6572  mapsncnv  6589  elixp2  6596  ixpin  6617  xpassen  6724  diffitest  6781  supmoti  6880  eqinfti  6907  distrnqg  7202  ltbtwnnq  7231  distrnq0  7274  nqprrnd  7358  ltresr  7654  elznn0nn  9075  xrnemnf  9571  xrnepnf  9572  elioomnf  9758  elxrge0  9768  elfzuzb  9807  fzass4  9849  elfz2nn0  9899  elfzo2  9934  elfzo3  9947  lbfzo0  9965  fzind2  10023  rexfiuz  10768  fisumcom2  11214  prodmodc  11354  infssuzex  11648  isbasis2g  12221  tgval2  12229  ntreq0  12310  txuni2  12434  isms2  12632  bdceq  13093
  Copyright terms: Public domain W3C validator