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

Theorem bitr4i 186
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 131 . 2  |-  ( ps  <->  ch )
41, 3bitri 183 1  |-  ( ph  <->  ch )
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:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  biancomi  268  imdistan  440  biadani  586  mpbiran  909  mpbiran2  910  3anrev  957  an6  1284  nfand  1532  19.33b2  1593  nf3  1632  nf4dc  1633  nf4r  1634  equsalh  1689  sb6x  1737  sb5f  1760  sbidm  1807  sb5  1843  sbanv  1845  sborv  1846  sbhb  1893  sb3an  1909  sbel2x  1951  sbal1yz  1954  sbexyz  1956  eu2  2021  2eu4  2070  cleqh  2217  cleqf  2282  dcne  2296  necon3bii  2323  ne3anior  2373  r2alf  2429  r2exf  2430  r19.23t  2516  r19.26-3  2539  r19.26m  2540  r19.43  2566  rabid2  2584  isset  2666  ralv  2677  rexv  2678  reuv  2679  rmov  2680  rexcom4b  2685  ceqsex4v  2703  ceqsex8v  2705  ceqsrexv  2789  ralrab2  2822  rexrab2  2824  reu2  2845  reu3  2847  reueq  2856  2reuswapdc  2861  reuind  2862  sbc3an  2942  rmo2ilem  2970  dfss2  3056  dfss3  3057  dfss3f  3059  ssabral  3138  rabss  3144  ssrabeq  3153  uniiunlem  3155  dfdif3  3156  ddifstab  3178  uncom  3190  inass  3256  indi  3293  difindiss  3300  difin2  3308  reupick3  3331  n0rf  3345  eq0  3351  eqv  3352  vss  3380  disj  3381  disj3  3385  undisj1  3390  undisj2  3391  exsnrex  3536  euabsn2  3562  euabsn  3563  prssg  3647  dfuni2  3708  unissb  3736  elint2  3748  ssint  3757  dfiin2g  3816  iunn0m  3843  iunxun  3862  iunxiun  3864  iinpw  3873  disjnim  3890  dftr2  3998  dftr5  3999  dftr3  4000  dftr4  4001  vnex  4029  inuni  4050  snelpw  4105  sspwb  4108  opelopabsb  4152  eusv2  4348  orddif  4432  onintexmid  4457  zfregfr  4458  tfi  4466  opthprc  4560  elxp3  4563  xpiundir  4568  elvv  4571  brinxp2  4576  relsn  4614  reliun  4630  inxp  4643  raliunxp  4650  rexiunxp  4651  cnvuni  4695  dm0rn0  4726  elrn  4752  ssdmres  4811  dfres2  4841  dfima2  4853  args  4878  cotr  4890  intasym  4893  asymref  4894  intirr  4895  cnv0  4912  xp11m  4947  cnvresima  4998  resco  5013  rnco  5015  coiun  5018  coass  5027  dfiota2  5059  dffun2  5103  dffun6f  5106  dffun4f  5109  dffun7  5120  dffun9  5122  funfn  5123  svrelfun  5158  imadiflem  5172  dffn2  5244  dffn3  5253  fintm  5278  dffn4  5321  dff1o4  5343  brprcneu  5382  eqfnfv3  5488  fnreseql  5498  fsn  5560  abrexco  5628  imaiun  5629  mpo2eqb  5848  elovmpo  5939  abexex  5992  releldm2  6051  fnmpo  6068  dftpos4  6128  tfrlem7  6182  0er  6431  eroveu  6488  erovlem  6489  map0e  6548  elixpconst  6568  domen  6613  reuen1  6663  xpf1o  6706  ssfilem  6737  finexdc  6764  ssfirab  6790  sbthlemi10  6822  djuexb  6897  dmaddpq  7155  dmmulpq  7156  distrnqg  7163  enq0enq  7207  enq0tr  7210  nqnq0pi  7214  distrnq0  7235  prltlu  7263  prarloc  7279  genpdflem  7283  ltexprlemm  7376  ltexprlemlol  7378  ltexprlemupu  7380  ltexprlemdisj  7382  recexprlemdisj  7406  ltresr  7615  elnnz  9022  dfz2  9081  2rexuz  9333  eluz2b1  9351  elxr  9518  elixx1  9635  elioo2  9659  elioopnf  9705  elicopnf  9707  elfz1  9750  fzdifsuc  9816  fznn  9824  fzp1nel  9839  fznn0  9848  redivap  10601  imdivap  10608  rexanre  10947  climreu  11021  3dvdsdec  11474  3dvds2dec  11475  bezoutlembi  11605  isprm2  11710  isprm3  11711  isprm4  11712  inffinp1  11853  isbasis3g  12124  restsn  12260  lmbr  12293  txbas  12338  tx2cn  12350  elcncf1di  12646  dedekindicclemicc  12690  limcrcl  12707  bj-nnor  12842  bj-vprc  12990  ss1oel2o  13085  subctctexmid  13092
  Copyright terms: Public domain W3C validator