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

Theorem bitr4i 180
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4i.1  |-  ( ph  <->  ps )
bitr4i.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
bitr4i  |-  ( ph  <->  ch )

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2  |-  ( ph  <->  ps )
2 bitr4i.2 . . 3  |-  ( ch  <->  ps )
32bicomi 127 . 2  |-  ( ps  <->  ch )
41, 3bitri 177 1  |-  ( ph  <->  ch )
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:  3bitr2i  201  3bitr2ri  202  3bitr4i  205  3bitr4ri  206  imdistan  426  mpbiran  858  mpbiran2  859  3anrev  906  an6  1227  nfand  1476  19.33b2  1536  nf3  1575  nf4dc  1576  nf4r  1577  equsalh  1630  sb6x  1678  sb5f  1701  sbidm  1747  sb5  1783  sbanv  1785  sborv  1786  sbhb  1832  sb3an  1848  sbel2x  1890  sbal1yz  1893  sbexyz  1895  eu2  1960  2eu4  2009  cleqh  2153  cleqf  2217  dcne  2231  necon3bii  2258  ne3anior  2308  r2alf  2358  r2exf  2359  r19.23t  2440  r19.26-3  2460  r19.26m  2461  r19.43  2485  rabid2  2503  isset  2578  ralv  2588  rexv  2589  reuv  2590  rmov  2591  rexcom4b  2596  ceqsex4v  2614  ceqsex8v  2616  ceqsrexv  2697  ralrab2  2729  rexrab2  2731  reu2  2752  reu3  2754  reueq  2761  2reuswapdc  2766  reuind  2767  sbc3an  2847  rmo2ilem  2875  dfss2  2962  dfss3  2963  dfss3f  2965  ssabral  3039  rabss  3045  ssrabeq  3054  uniiunlem  3056  uncom  3115  inass  3175  nsspssun  3198  indi  3212  difindiss  3219  difin2  3227  reupick3  3250  n0rf  3261  eq0  3267  eqv  3268  vss  3292  disj  3296  disj3  3300  undisj1  3307  undisj2  3308  exsnrex  3441  euabsn2  3467  euabsn  3468  prssg  3549  dfuni2  3610  unissb  3638  elint2  3650  ssint  3659  dfiin2g  3718  iunn0m  3745  iunxun  3763  iunxiun  3764  iinpw  3770  dftr2  3884  dftr5  3885  dftr3  3886  dftr4  3887  vprc  3916  inuni  3937  snelpw  3977  sspwb  3980  opelopabsb  4025  eusv2  4217  orddif  4299  onintexmid  4325  zfregfr  4326  tfi  4333  opthprc  4419  elxp3  4422  xpiundir  4427  elvv  4430  brinxp2  4435  relsn  4471  reliun  4486  inxp  4498  raliunxp  4505  rexiunxp  4506  cnvuni  4549  dm0rn0  4580  elrn  4605  ssdmres  4661  dfres2  4686  dfima2  4698  args  4722  cotr  4734  intasym  4737  asymref  4738  intirr  4739  cnv0  4755  xp11m  4787  cnvresima  4838  resco  4853  rnco  4855  coiun  4858  coass  4867  dfiota2  4896  dffun2  4940  dffun6f  4943  dffun4f  4946  dffun7  4956  dffun9  4958  funfn  4959  svrelfun  4992  imadiflem  5006  dffn2  5075  dffn3  5081  fintm  5103  dffn4  5140  dff1o4  5162  brprcneu  5199  eqfnfv3  5295  fnreseql  5305  fsn  5363  abrexco  5426  imaiun  5427  mpt22eqb  5638  elovmpt2  5729  abexex  5781  releldm2  5839  fnmpt2  5856  dftpos4  5909  tfrlem7  5964  0er  6171  eroveu  6228  erovlem  6229  domen  6263  reuen1  6312  ssfiexmid  6367  dmaddpq  6535  dmmulpq  6536  distrnqg  6543  enq0enq  6587  enq0tr  6590  nqnq0pi  6594  distrnq0  6615  prltlu  6643  prarloc  6659  genpdflem  6663  ltexprlemm  6756  ltexprlemlol  6758  ltexprlemupu  6760  ltexprlemdisj  6762  recexprlemdisj  6786  ltresr  6973  elnnz  8312  dfz2  8371  2rexuz  8621  eluz2b1  8635  elxr  8797  elixx1  8867  elioo2  8891  elioopnf  8937  elicopnf  8939  elfz1  8981  fzdifsuc  9045  fznn  9053  fzp1nel  9068  fznn0  9076  redivap  9702  imdivap  9709  climreu  10049  3dvdsdec  10176  3dvds2dec  10177  dcdc  10288  bj-vprc  10403
  Copyright terms: Public domain W3C validator