Theorem bitr4i 193

Description: An inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
bitr4i.1	|- (ph <-> ps)
bitr4i.2	|- (ch <-> ps)

Assertion

Ref	Expression
bitr4i	|- (ph <-> ch)

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 |- (ph <-> ps)
2		bitr4i.2	. . 3 |- (ch <-> ps)
3	2	bicomi 189	. 2 |- (ps <-> ch)
4	1, 3	bitri 190	1 |- (ph <-> ch)

Syntax hints:   <-> wb 163

This theorem is referenced by:  3bitr2i 196  3bitr2ri 197  3bitr4i 200  3bitr4ri 201  imor 251  oridmOLD 263  ianorOLD 330  ioran 331  ioranOLD 332  pm4.52 333  pm4.54 335  pm4.79 382  dfbi2 572  bibi2iOLD 670  pm5.32 706  pm5.6 752  mpbiran 798  mpbiran2 799  biluk 817  prlem2OLD 851  3anrev 868  3ianorOLD 871  an6 1177  nic-justbi 1234  nic-ax 1239  nic-axALT 1240  impexp3acom3r 1294  19.33bOLD 1445  19.41OLD 1449  equsal 1511  equsalOLD 1512  sb6x 1553  sb5f 1571  sb3an 1608  sbequ8 1618  hbsb4tOLD 1622  sb5 1645  sbhb 1714  sbel2x 1736  eu2 1791  eu3 1792  eu5 1805  moanim 1826  euanOLD 1828  2eu4 1856  2eu6 1858  cleqf 1984  necon3bii 2032  neor 2096  neorian 2098  r2al 2136  r2ex 2152  r19.23OLD 2207  r19.26m 2222  r19.27avOLD 2225  r19.29OLD 2228  r19.43 2238  2ralor 2250  rabid2 2254  rabid2OLD 2255  isset 2296  ralv 2305  rexv 2306  reuv 2307  ceqsex4v 2331  ceqsex8v 2333  ceqsrexv 2394  ralrab 2418  reu2 2442  reu6 2443  reu3 2444  2reuswap 2449  reuind 2450  elrabsf 2486  difjustOLD 2596  unjustOLD 2599  injustOLD 2602  dfss2 2610  dfss3 2611  dfss3f 2613  nss 2670  ssabral 2678  rabss 2684  sspsstri 2711  difdif 2734  uncom 2744  unassOLD 2760  unss 2780  rexun 2783  inass 2804  dfss4 2827  indi 2838  unabOLD 2860  inabOLD 2862  difab 2863  ne0f 2883  eqv 2890  vss 2908  disj 2914  reldisjOLD 2917  disj3 2918  undisj1 2925  undisj2 2926  ssdif0 2934  inundif 2951  undif 2954  snjustOLD 3048  eltp 3074  ralprOLDOLD 3081  pwpw0 3134  prssg 3140  dfuni2 3179  unissb 3208  elint2 3221  ssint 3232  dfiin2g 3286  dfiin2OLD 3288  iunssOLD 3292  iinssOLD 3305  iunn0 3315  iunn0OLD 3316  iundif2 3322  iindif2 3324  iunxun 3329  iinpw 3336  dftr2 3413  dftr5 3414  dftr3 3415  dftr4 3416  truni 3425  vprc 3449  inuni 3470  notzfaus 3478  snelpw 3501  sspwb 3503  nssss 3509  opabidOLD 3558  pwssun 3578  dfid3 3587  posn 3603  dffr2 3627  dffr2OLD 3628  ordtri4OLD 3700  dflim2 3719  orddif 3764  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq2 3829  eufromeq4 3831  eufromeq6 3833  euobj2 3835  onzslOLD 3929  opthprc 4046  elxp3 4049  elvv 4053  reliun 4101  inxp 4109  cnvcoOLD 4146  cnvuni 4147  dmuni 4166  dmxpOLD 4178  elrn 4197  dmres 4234  ssdmres 4235  dfima2 4265  dfima2OLD 4266  args 4293  dffr3 4297  cotr 4302  cotrOLD 4303  intasym 4306  intasymOLD 4307  asymref 4308  asymrefOLD 4309  intirrOLD 4313  cnvopabOLD 4318  cnv0 4319  cnvunOLD 4323  cnvin 4324  rnuni 4327  xpnz 4335  xp11 4347  coresOLD 4401  resco 4402  imaco 4403  rnco 4404  coiun 4407  coass 4415  cnvpo 4427  cnvso 4428  dffun2 4431  dffun6f 4435  dffun7 4447  funfn 4451  svrelfun 4478  fununi 4481  funinOLD 4485  iunfopabOLD 4543  dffn2 4563  dffn3 4570  fint 4591  fintOLD 4592  dffn4 4623  dff1o2 4639  dff1o4 4644  dff1o4OLD 4645  dff1o5OLD 4647  f1ocnvOLD 4652  fv2 4676  eqfnfv3 4769  fsn 4807  abexex 4849  dff13 4850  elxp6 5041  elxp7 5042  fnoprab2g 5063  onopriun 5118  tfrlem5 5123  tfrlem7 5125  dfrdg2 5141  rdgsucopabn 5155  2onOLD 5184  eqerlem 5328  qsid 5360  elixpconst 5410  domen 5438  brsdom 5440  brdom2 5447  sbthlem10 5519  sbthcl 5522  brsdom2 5524  xpmapenlem5 5594  mapunen 5596  unfi 5644  ordtypelem7 5690  trcl 5752  zfregs 5754  tz9.12lem3 5772  rankr1 5785  rankss 5799  cplem1 5850  aceq0 5892  aceq3lem 5894  aceq5lem2 5898  aceq5 5902  aceq7 5905  kmlem12 5938  kmlem14 5940  kmlem15 5941  zorn 5959  brdom7disj 5966  entri2 5991  unxpdomlem 5995  cardval2 6007  isinfcard 6035  iscard3 6036  elni2 6157  distrpq 6219  psslinpr 6287  ltexprlem4 6297  ltresr 6410  subaddi 6528  elxr 6706  divmuli 6894  prodge0i 6998  ltdiv1ii 7001  infm3 7263  xrinfmss 7288  dfn2 7321  elnnz 7354  elznn0nn 7357  elnn0nn 7380  elioo1 7545  elioo2 7546  elioc1 7548  elico1 7549  elicc1 7550  snunioolem 7583  2rexuz 7615  nnwos 7629  elfz1 7640  elfzuzb 7646  elfz2nn0 7667  fznn0 7694  fznn 7695  seq1lem2 7723  discrlem1 7906  nn0opthlem1 7914  creur 7992  creui 7993  cvg3i 8175  faclbnd4lem1 8200  climreu 8361  isumclimtfi 8456  infcvglem1 8482  elcncf1di 8532  reefiso 8693  qnnen 8772  infxpidmlem2 8822  infxpidmlem7 8827  infxpidmlem8 8828  infmap2 8850  isbasis3g 8882  tgval2 8887  fctop 8920  cctop 8922  ntreq0 8984  islp2 9023  blfval2 9113  metcnp4 9248  xpcn 9254  fsumcnlem 9267  bcthlem9 9285  bcthlem14 9290  nmobndseqi 9780  pilem3 10022  efif1lem5 10088  axgroth4 10139  grothprim 10141  rexcom4b 10148  symgoprab 10201  abfi 10215  fbunfip 10282  extbas1 10291  filrn 10293  filmapf 10307  hcau2 10688  ocsh 10789  projlem4 10822  spanuni 11100  nonbooli 11231  5oalem7 11240  adjsym 11396  elbdop2 11435  dmadjss 11456  eleigvec 11518  nmop0h 11553  nmcopexlem1 11588  nmcfnexlem1 11617  rnbra 11678  pjssposi 11744  pjordi 11745  cvbr2 11855  cvnbtwn2 11859  mdsl2i 11894  cvmdi 11896  elat2 11912  atom1d 11925  chrelat2i 11937  irredi 11966  cdj3i 12013  bnj208OLD 12052  bnj252 12091  bnj253 12092  bnj254 12093  bnj255 12094  bnj345 12187  bnj367OLD 12211  bnj14 12381  bnj14OLD 12382  bnj19 12385  bnj28 12391  bnj30 12395  bnj30OLD 12396  bnj100 12449  bnj99 12450  bnj131 12462  bnj131OLD 12463  bnj133 12466  bnj537 12533  bnj538 12534  bnj856 12789  bnj899 12816  bnj901 12818  bnj962 12856  bnj971 12860  bnj997 12873  bnj1046 12887  bnj1054 12891  bnj1055 12892  bnj1056 12893  bnj1061 12898  bnj1076 12904  bnj1086 12908  bnj1163 12955  bnj1194 12971  bnj1215 12991  bnj1267 13026  bnj1331 13062  bnj1524 13177  bnj70 13205  bnj85 13212  bnj114 13227  bnj119 13229  bnj121 13231  bnj130 13240  bnj581 13294  bnj582 13295  bnj607 13304  bnj849 13318  bnj889 13323  bnj917 13333  bnj934 13334  bnj983 13357  bnj987 13361  bnj1033 13384  bnj1045 13392  bnj1047 13393  bnj1049 13394  bnj1067 13399  bnj1069 13400  bnj1070 13401  bnj1081 13407  bnj1128 13428  bnj1253 13470  dvdslelem 13692  divalglem10 13705  algcvgblem 13745  zgt1b2 13772  isprm2 13775  isprm3 13776  truniOLD 13792  nepss 13820  indifdi 13823  dffr5 13831  elpotr 13847  dfon2lem3 13851  dfon2lem5 13853  dfon2lem7 13855  dfon2lem8 13856  predreseq 13890  cbvsetlike 13892  dffr4 13893  frsucopabn 13911  wfi 13915  frind 13939  frxp 13951  soseq 13955  wfrlem5 13961  wfrlem8 13964  wfrlem11 13967  nosgnn0 13999  nocvxminlem 14028  axfelem9 14039  axfelem11 14041  eltrans 14071  dfon3 14072  altxpsspw 14100  df3nandALT1 14146  df3nandALT2 14147  r19.26t 14282  ficli 14353  hmeogrp 14892  sbtpsines 14905  cnfilca 14927  limvinlv 14941  tmpts 15257  isline1 15294  dfiin2gOLD 15356  cnvresima 15359  ordtypelem7OLD 15381  hscptsscld 15434  alexsublem3 15439  alexsublem4 15440  dfcon2 15442  neibastop1 15518  ist1-3 15543  fbasfip 15556  neifg 15559  filfinnfr 15561  filssufillem 15570  fixufil 15576  ufinffr 15578  rnelfmlem 15592  fmfnfmlem3 15596  filnetlem3 15642  2ralorOLD 15655  rexunOLD 15656  rexcom4bOLD 15660  ralrabOLD 15670  difin2 15676  eqfnfv3OLD 15721  eroprlem 15732  fimax2g 15769  fzsplit 15792  sdc 15811  fdc 15812  nninfnub 15819  pi1val 16094  pi1gp 16095  isdivrng1 16109  ispridl 16182  ismaxidl 16188  prtlem70 16238  prtlem5 16245  prtlem16 16272  2exnaln 16326  2nalexn 16340  2exnexn 16341  pm11.52 16342  pm11.58 16347  elnev 16404  compel 16415  conss34 16419  undif3VD 16706  elstr2 16718  eustrdif2 16723  stb2el 16733  stb2cl 16734  stb2val1 16735  stb2val2 16736  stb3el 16737  stb3cl 16738  stb3val1 16739  stb3val2 16740  stb3val3 16741  isposNEW 16773  isopos 16909  cvrval2 16991  cvrnbtwn3 16993  ishlat 17018  hlrelat2 17052  cvrat4 17076  isgrpNEW 17104  isringNEW 17142  pmapglbx 17251

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain