Theorem bitrd 406

Description: Deduction form of bitr 151.

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 135	. . 3 |- (ph -> (ps -> ch))
3		bitrd.2	. . 3 |- (ph -> (ch <-> th))
4	2, 3	sylibd 177	. 2 |- (ph -> (ps -> th))
5	3	biimprd 136	. . 3 |- (ph -> (th -> ch))
6	5, 1	sylibrd 179	. 2 |- (ph -> (th -> ps))
7	4, 6	impbid 397	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bitr2d 407  bitr3d 408  bitr4d 409  syl5bb 410  syl6bb 414  sylan9bb 418  3bitrd 422  3bitr3d 423  3bitr4d 424  bibi2d 470  imbi12d 474  orbi12d 475  anbi12d 476  bibi12d 477  dedlem0a 567  dedlema 569  cleq12d 1115  eleq12d 1157  raleqd 1327  rexeqd 1328  reueqd 1329  elrabsf 1456  nalset 1482  sseq12d 1529  psseq12d 1566  raaan 1775  dedth2v 1785  elimhyp2v 1791  copsex4g 1904  treq 2047  breq12d 2073  efrirr 2180  limeq 2211  ordtri1 2231  onpwsuc 2315  dfom2 2374  findsg 2398  tfindsg 2402  vtoclrbr 2450  vtoclibr 2451  brinxp 2466  resieq 2581  fconst 2774  fniunfv 2860  dmfco 2864  fvopabn 2873  fressnfv 2898  isomin 2937  isoini 2938  isowe 2941  f1oiso 2942  f1oweOLD 2944  oprabval 3047  oaord1 3153  nnaordr 3178  nnaordex 3191  nnawordex 3192  ereq 3206  erref 3212  brecop 3242  eceqopreq 3249  dom2d 3307  xpdom2 3345  sbthlem2 3350  sbth 3359  nndomo 3416  unfilem2 3439  unfilem3 3440  eirr 3450  inf5 3472  r1pw 3529  aceq6b 3565  kmlem2 3581  iscard2 3660  axpownd 3747  ltapi 3824  ltmpi 3825  nlt1pi 3827  indpi 3828  enqeceq 3841  ltapq 3870  genpass 3906  mulclprlem 3915  distrlem1pr 3921  distrlem5pr 3925  1idpr 3927  prlem936b 3948  prlem936 3949  reclem4pr 3953  enreceq 3971  addgt0sr 4007  sqgt0sr 4009  ltresr 4052  leloet 4284  lenltt 4285  ltadd2t 4349  leadd2t 4351  ltaddsub2t 4358  ltaddpost 4363  ltnegcon1t 4367  lenegcon1t 4369  ltmuldiv 4400  nnleltp1t 4448  nnreclt 4522  nn0ltlem1 4558  nn0subt 4587  znnsubt 4595  zltp1let 4597  uzind 4603  uzwo 4605  nnwoOLD 4608  nn0ennn 4925  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem11 4943  norm-it 5080  projlem2 5194  chsscon1t 5418  chsscon2t 5419  chpsscon1t 5421  chpsscon2t 5422  chlejb2t 5430  elspansn2t 5472  mdbr2 5728  mdbr3 5729  mdbr4 5730  dmdbr 5731  dmdbr2 5733  atnssm0 5765  atcvatlem 5770  sumdmdi 5785

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org