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  imdistan  438  biadani  584  mpbiran  907  mpbiran2  908  3anrev  955  an6  1282  nfand  1530  19.33b2  1591  nf3  1630  nf4dc  1631  nf4r  1632  equsalh  1687  sb6x  1735  sb5f  1758  sbidm  1805  sb5  1841  sbanv  1843  sborv  1844  sbhb  1891  sb3an  1907  sbel2x  1949  sbal1yz  1952  sbexyz  1954  eu2  2019  2eu4  2068  cleqh  2215  cleqf  2280  dcne  2294  necon3bii  2321  ne3anior  2371  r2alf  2427  r2exf  2428  r19.23t  2514  r19.26-3  2537  r19.26m  2538  r19.43  2564  rabid2  2582  isset  2664  ralv  2675  rexv  2676  reuv  2677  rmov  2678  rexcom4b  2683  ceqsex4v  2701  ceqsex8v  2703  ceqsrexv  2787  ralrab2  2820  rexrab2  2822  reu2  2843  reu3  2845  reueq  2854  2reuswapdc  2859  reuind  2860  sbc3an  2940  rmo2ilem  2968  dfss2  3054  dfss3  3055  dfss3f  3057  ssabral  3136  rabss  3142  ssrabeq  3151  uniiunlem  3153  dfdif3  3154  ddifstab  3176  uncom  3188  inass  3254  indi  3291  difindiss  3298  difin2  3306  reupick3  3329  n0rf  3343  eq0  3349  eqv  3350  vss  3378  disj  3379  disj3  3383  undisj1  3388  undisj2  3389  exsnrex  3534  euabsn2  3560  euabsn  3561  prssg  3645  dfuni2  3706  unissb  3734  elint2  3746  ssint  3755  dfiin2g  3814  iunn0m  3841  iunxun  3860  iunxiun  3862  iinpw  3871  disjnim  3888  dftr2  3996  dftr5  3997  dftr3  3998  dftr4  3999  vnex  4027  inuni  4048  snelpw  4103  sspwb  4106  opelopabsb  4150  eusv2  4346  orddif  4430  onintexmid  4455  zfregfr  4456  tfi  4464  opthprc  4558  elxp3  4561  xpiundir  4566  elvv  4569  brinxp2  4574  relsn  4612  reliun  4628  inxp  4641  raliunxp  4648  rexiunxp  4649  cnvuni  4693  dm0rn0  4724  elrn  4750  ssdmres  4809  dfres2  4839  dfima2  4851  args  4876  cotr  4888  intasym  4891  asymref  4892  intirr  4893  cnv0  4910  xp11m  4945  cnvresima  4996  resco  5011  rnco  5013  coiun  5016  coass  5025  dfiota2  5057  dffun2  5101  dffun6f  5104  dffun4f  5107  dffun7  5118  dffun9  5120  funfn  5121  svrelfun  5156  imadiflem  5170  dffn2  5242  dffn3  5251  fintm  5276  dffn4  5319  dff1o4  5341  brprcneu  5380  eqfnfv3  5486  fnreseql  5496  fsn  5558  abrexco  5626  imaiun  5627  mpo2eqb  5846  elovmpo  5937  abexex  5990  releldm2  6049  fnmpo  6066  dftpos4  6126  tfrlem7  6180  0er  6429  eroveu  6486  erovlem  6487  map0e  6546  elixpconst  6566  domen  6611  reuen1  6661  xpf1o  6704  ssfilem  6735  finexdc  6762  ssfirab  6788  sbthlemi10  6820  djuexb  6895  dmaddpq  7151  dmmulpq  7152  distrnqg  7159  enq0enq  7203  enq0tr  7206  nqnq0pi  7210  distrnq0  7231  prltlu  7259  prarloc  7275  genpdflem  7279  ltexprlemm  7372  ltexprlemlol  7374  ltexprlemupu  7376  ltexprlemdisj  7378  recexprlemdisj  7402  ltresr  7611  elnnz  9015  dfz2  9074  2rexuz  9326  eluz2b1  9344  elxr  9503  elixx1  9620  elioo2  9644  elioopnf  9690  elicopnf  9692  elfz1  9735  fzdifsuc  9801  fznn  9809  fzp1nel  9824  fznn0  9833  redivap  10586  imdivap  10593  rexanre  10932  climreu  11006  3dvdsdec  11458  3dvds2dec  11459  bezoutlembi  11589  isprm2  11694  isprm3  11695  isprm4  11696  inffinp1  11837  isbasis3g  12108  restsn  12244  lmbr  12277  txbas  12322  tx2cn  12334  elcncf1di  12630  limcrcl  12670  bj-nnor  12748  bj-vprc  12896  ss1oel2o  12991  subctctexmid  12998
  Copyright terms: Public domain W3C validator