Theorem bitrd 528

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 516	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  bitr2d 529  bitr3d 530  bitr4d 531  syl5bb 532  syl6bb 536  sylan9bb 540  3bitrd 544  3bitr2d 546  3bitr3d 548  3bitr4d 550  bibi2d 618  imbi12d 626  orbi12d 627  anbi12d 628  bibi12d 629  dedlem0a 760  dedlema 762  ax11el 1364  eqeq12d 1489  eleq12d 1542  raleqd 1791  rexeqd 1792  reueqd 1793  raleq12d 1794  rexeq12d 1795  elrabsf 1963  sbcth2 1982  hbsbcgd 1984  sbc19.21g 1987  sbcralt 1990  sbcrext 1991  sbcralgf 1992  sbcrexgf 1993  sbcabel 1996  ra4sbc 1997  csbcog 2007  sbcel12g 2011  sbcel1g 2013  sbceq1dig 2014  sbcel2g 2015  sbceq2dig 2016  sbcco3g 2041  sseq12d 2090  psseq12d 2142  raaan 2360  dedth2v 2384  dedth4v 2386  elimhyp2v 2391  elimhyp4v 2393  keephyp2v 2397  breq12d 2631  hbbrd 2659  sbcbrg 2662  sbcbr12g 2663  sbcbr1g 2664  sbcbr2g 2665  csbopabg 2678  treq 2686  nalset 2712  copsex4g 2794  opelopab2 2819  elpwun 2911  efrirr 2928  limeq 2960  ordtri1 2980  ordpwsuc 3066  ordunisuc2 3115  dfom2 3133  findsg 3157  tfindsg 3162  vtoclrbr 3212  vtoclibr 3213  ididg 3278  fconst 3658  fnrnfv 3759  dmfco 3773  fvopabn 3786  funimass3 3806  funconstss 3808  dffo3 3819  fressnfv 3838  f1ofveu 3882  isomin 3899  isoini 3900  isowe 3903  f1oiso 3904  f1oweALT 3906  oprabval 4023  dfopab2 4113  dfoprab3 4114  oe0m1 4160  oaord1 4185  omord 4199  omlimcl 4209  oewordi 4218  nnaordr 4236  nnaordex 4249  nnawordex 4250  ereq 4267  erref 4275  brecop 4306  eceqopreq 4313  elmapg 4333  dom2d 4404  sbthlem2 4448  sbth 4457  nndomo 4521  unfilem2 4549  unfilem3 4550  elirr 4599  infeq5 4621  r1pw 4686  rankxplim 4712  aceq6b 4742  kmlem2 4766  brdom7disj 4804  brdom6disj 4805  unidom 4808  iscard2 4854  axpownd 4953  ltapi 5030  ltmpi 5031  nlt1pi 5033  indpi 5034  enqeceq 5047  ltapq 5076  genpass 5112  mulclprlem 5121  distrlem1pr 5127  distrlem5pr 5131  1idpr 5133  prlem936b 5154  prlem936 5155  reclem4pr 5159  enreceq 5177  addgt0sr 5213  sqgt0sr 5215  ltresr 5258  cnegextlem1 5345  ltxrt 5495  ltxrltt 5500  leloet 5518  eqleltt 5519  xrleloet 5557  ltadd2t 5624  leadd2t 5626  ltaddsub2t 5632  leaddsub2t 5634  ltaddpost 5651  ltnegcon1t 5656  lenegcon1t 5658  lenegcon2t 5659  lesub1t 5660  ltsub1t 5662  addge01t 5672  addge02t 5673  mulcan2t 5692  mulcan2tOLD 5693  divmul3t 5709  ltmuldiv 5825  ltmul2t 5831  lemul2t 5833  ltmulgt11t 5846  ltmulgt12t 5847  gt0divt 5853  ge0divt 5854  ltdivmul2tOLD 5871  ledivmul2tOLD 5873  ltdiv2t 5887  ltrec1t 5888  lerec2t 5889  ledivdivt 5890  ltdiv23t 5892  lediv23t 5893  nnleltp1t 5954  nnreclt 6072  supxrre2 6094  nn0subt 6161  znnsubt 6177  zltp1let 6181  btwnnzt 6192  gtndivt 6193  uzindOLD 6208  uzwo4OLD 6210  flval3t 6239  btwnzge0t 6245  ioo0t 6368  elioo3g 6380  icoshftf1olem 6410  icounlem 6412  eluz2t 6421  uzwo 6455  uzwoOLD 6456  elfz2t 6472  fzsubelt 6501  fzrevral2t 6520  fzrevral3t 6521  fzshftralt 6522  expeq0t 6585  sq01t 6651  absrpclt 6855  absdifltt 6883  absdiflet 6884  lenegsqt 6885  dffsum 6998  fsum1s2 7010  clm0 7083  clm0nns 7085  climshft2 7106  caucvg 7163  dfisum 7191  efcltlem1 7304  reeff1o 7426  efieq 7450  nn0ennn 7497  infxpidmlem2 7553  infxpidmlem3 7554  infxpidmlem11 7562  eltgt 7618  eltg2t 7619  iscld 7669  iscld4 7696  elcls2 7705  elcls3 7711  isnei 7718  islp2 7747  cldlp 7750  iscn 7758  iscnp 7760  iscnp2 7761  iscncl 7770  cncnp2 7779  sncld 7787  ismet 7798  metne0 7821  metreslem 7822  metxp 7834  elbl3 7840  blrn 7841  isopn 7859  isopn4 7862  metcnplem 7886  metcnp 7887  metcnp2 7888  metcn 7889  metcnp3 7896  cncfmet 7905  bl2ioo 7911  ioo2bl 7912  lmbrf 7930  iscau 7936  iscau5 7941  iscaunns 7944  lmclim 7963  metcnp4 7970  metcn4 7971  cncms 7998  bcthlem1 7999  bcthlem25 8023  isgrp 8041  grplactf1o 8098  isabl 8101  isring 8141  ringi 8142  vci 8167  isvclem 8196  vcoprnelem 8197  nvsubadd 8275  nvelbl 8325  nvelbl2 8326  nmo0 8451  blocnilem 8464  isph 8481  spwpr3OLD 8662  pilem3 8673  sincosq2sgn 8705  sinq12gt0t 8708  efifolem6 8727  efifolem7 8728  eff1i 8744  logltbt 8776  h2hlm 8850  hvaddeq0t 8936  hial2eq2t 8973  norm-it 8996  hhcms 9072  hhssnv 9134  hhsscms 9150  projlem2 9187  pjeqt 9242  shsel3t 9279  chssoct 9419  chsscon1t 9424  chsscon2t 9425  chpsscon1t 9427  chpsscon2t 9428  chlejb2t 9436  elspansn2t 9490  fh1t 9561  fh2t 9562  cm2jt 9563  eigpos 9762  unopf1ot 9840  nmcopexlem3 9953  lnopcnret 9968  nmcfnexlem3 9982  riesz4 9996  leop2t 10057  leop3t 10058  leoppost 10059  hst1ht 10154  mdbr2 10223  mdbr3 10224  mdbr4 10225  dmdbr2 10230  dmdbr3 10232  dmdbr4 10233  mddmd 10236  cvdmdt 10264  atcvatlem 10312  atdmd 10325  sumdmdi 10342  dmdbr5at 10349  cdj3lem1 10361  elghomlem2 10383  symgval 10403  nndivlub 10422  elo 10444  sppfi 10486  sppfiOLD 10487  cdrci 10494  ishomeo 10517  cnfilca 10583  cnfilcaOLD 10584  iintlem1 10632  ismgra 10642  isalg 10653  algi 10660  ismonb 10738  ismonc 10742  isepib 10748  isfunb 10755  hgrablkcard 10774

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