Theorem bitrd 526

Description: Deduction form of bitr 173.

Hypotheses

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

Assertion

Ref	Expression
bitrd	|- (ph -> (ps <-> th))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	biimpd 153	. . 3 |- (ph -> (ps -> ch))
3		bitrd.2	. . 3 |- (ph -> (ch <-> th))
4	2, 3	sylibd 202	. 2 |- (ph -> (ps -> th))
5	3	biimprd 154	. . 3 |- (ph -> (th -> ch))
6	5, 1	sylibrd 204	. 2 |- (ph -> (th -> ps))
7	4, 6	impbid 514	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  bitr2d 527  bitr3d 528  bitr4d 529  syl5bb 530  syl6bb 534  sylan9bb 538  3bitrd 542  3bitr2d 544  3bitr3d 546  3bitr4d 548  bibi2d 616  imbi12d 624  orbi12d 625  anbi12d 626  bibi12d 627  dedlem0a 758  dedlema 760  ax11el 1357  eqeq12d 1481  eleq12d 1534  raleqd 1783  rexeqd 1784  reueqd 1785  raleq12d 1786  rexeq12d 1787  elrabsf 1953  sbcth2 1972  hbsbcgd 1974  sbc19.21g 1977  sbcralt 1980  sbcrext 1981  sbcralgf 1982  sbcrexgf 1983  sbcabel 1986  ra4sbc 1987  csbcog 1997  sbcel12g 2001  sbcel1g 2003  sbceq1dig 2004  sbcel2g 2005  sbceq2dig 2006  sbcco3g 2031  sseq12d 2080  psseq12d 2132  raaan 2350  dedth2v 2374  dedth4v 2376  elimhyp2v 2381  elimhyp4v 2383  keephyp2v 2387  breq12d 2621  hbbrd 2649  sbcbrg 2652  sbcbr12g 2653  sbcbr1g 2654  sbcbr2g 2655  csbopabg 2668  treq 2676  nalset 2702  copsex4g 2784  opelopab2 2808  elpwun 2901  efrirr 2918  limeq 2950  ordtri1 2970  ordpwsuc 3056  ordunisuc2 3105  dfom2 3123  findsg 3147  tfindsg 3152  vtoclrbr 3202  vtoclibr 3203  ididg 3268  fconst 3643  fnrnfv 3744  dmfco 3758  fvopabn 3771  funimass3 3791  funconstss 3793  dffo3 3804  fressnfv 3823  f1ofveu 3867  isomin 3884  isoini 3885  isowe 3888  f1oiso 3889  f1oweALT 3891  oprabval 4008  dfopab2 4097  dfoprab3 4098  oe0m1 4144  oaord1 4169  omord 4183  omlimcl 4193  oewordi 4202  nnaordr 4220  nnaordex 4233  nnawordex 4234  ereq 4251  erref 4259  brecop 4290  eceqopreq 4297  elmapg 4317  dom2d 4385  sbthlem2 4428  sbth 4437  nndomo 4500  unfilem2 4525  unfilem3 4526  elirr 4571  infeq5 4593  r1pw 4658  rankxplim 4684  aceq6b 4714  kmlem2 4738  brdom7disj 4776  brdom6disj 4777  unidom 4780  iscard2 4826  axpownd 4925  ltapi 5002  ltmpi 5003  nlt1pi 5005  indpi 5006  enqeceq 5019  ltapq 5048  genpass 5084  mulclprlem 5093  distrlem1pr 5099  distrlem5pr 5103  1idpr 5105  prlem936b 5126  prlem936 5127  reclem4pr 5131  enreceq 5149  addgt0sr 5185  sqgt0sr 5187  ltresr 5230  cnegextlem1 5317  ltxrt 5467  ltxrltt 5472  leloet 5491  eqleltt 5492  xrleloet 5530  ltadd2t 5598  leadd2t 5600  ltaddsub2t 5606  leaddsub2t 5608  ltaddpost 5624  ltnegcon1t 5629  lenegcon1t 5631  lenegcon2t 5632  lesub1t 5633  ltsub1t 5635  addge01t 5645  addge02t 5646  mulcan2t 5662  divmul3t 5678  ltmuldiv 5781  ltmul2t 5787  lemul2t 5789  ltmulgt11t 5802  ltmulgt12t 5803  gt0divt 5807  ge0divt 5808  ltdivmul2t 5821  ledivmul2t 5823  ltdiv2t 5835  ltrec1t 5836  lerec2t 5837  ledivdivt 5838  ltdiv23t 5840  lediv23t 5841  nnleltp1t 5901  nnreclt 6019  supxrre2 6041  nn0subt 6108  znnsubt 6124  zltp1let 6128  btwnnzt 6139  gtndivt 6140  uzindOLD 6156  uzwo4OLD 6158  flval3t 6182  btwnzge0t 6188  ioo0t 6305  elioo3g 6317  icoshftf1olem 6343  icounlem 6345  eluz2t 6353  uzwo 6387  uzwoOLD 6388  elfz2t 6404  fzsubelt 6433  fzrevral2t 6452  fzrevral3t 6453  fzshftralt 6454  expeq0t 6517  sq01t 6582  crutOLD 6669  absrpclt 6790  absdifltt 6821  absdiflet 6822  lenegsqt 6823  dffsum 6936  fsum1s2 6948  clm0 7021  clm0nns 7023  climshft2 7043  caucvg 7099  dfisum 7127  efcltlem1 7246  reeff1o 7368  efieq 7392  nn0ennn 7439  infxpidmlem2 7496  infxpidmlem3 7497  infxpidmlem11 7505  eltgt 7560  eltg2t 7561  iscld 7611  iscld4 7638  elcls2 7647  elcls3 7652  isnei 7659  islp2 7688  iscn 7698  iscnp 7700  iscncl 7709  cncnp2 7718  sncld 7726  ismet 7737  metreslem 7762  metxp 7774  elbl3 7780  blrn 7781  isopn 7799  isopn4 7802  metcnplem 7825  metcnp 7826  metcnp2 7827  metcn 7828  metcnp3 7835  cncfmet 7844  bl2ioo 7850  ioo2bl 7851  lmbrf 7868  iscau 7874  iscau5 7878  lmclim 7898  metcnp4 7904  metcn4 7905  cncms 7932  bcthlem1 7933  bcthlem25 7957  isgrp 7975  grplactf1o 8034  isabl 8037  isring 8078  ringi 8079  vci 8104  isvcgOLD 8133  isvclem 8134  vcoprnelem 8135  nvsubadd 8215  nvelbl 8263  nvelbl2 8264  nmo0 8383  blocnilem 8395  isph 8412  pilem3 8592  sincosq2sgn 8622  sinq12gt0t 8625  efifolem6 8642  efifolem7 8643  eff1i 8665  logltbt 8698  h2hlm 8789  hvaddeq0t 8857  hial2eq2t 8894  norm-it 8917  hhcms 8993  hhssnv 9054  hhsscms 9067  projlem2 9103  pjeqt 9157  shsel3t 9194  chssoct 9334  chsscon1t 9339  chsscon2t 9340  chpsscon1t 9342  chpsscon2t 9343  chlejb2t 9351  elspansn2t 9406  fh1t 9478  fh2t 9479  cm2jt 9480  eigpos 9679  unopf1ot 9756  nmcopexlem3 9868  lnopcnret 9883  nmcfnexlem3 9897  riesz4 9911  leop2t 9969  leop3t 9970  leoppost 9971  hst1ht 10064  mdbr2 10133  mdbr3 10134  mdbr4 10135  dmdbr2 10140  dmdbr3 10141  dmdbr4 10142  mddmd 10144  cvdmdt 10172  atcvatlem 10220  atdmd 10233  sumdmdi 10249  dmdbr5at 10255  cdj3lem1 10266  elghomlem2 10288  symgval 10308  elo 10345  sppfi 10376  cdrci 10381  ishomeo 10404  cnfilca 10451  iintlem1 10476  ismgra 10486  isalg 10497  algi 10504  ismonb 10580  ismonc 10584  isfunb 10593  hgrablkcard 10610

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 147  df-an 225

Copyright terms: Public domain