Theorem bitrd 531

Description: Deduction form of bitri 171.

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 151	. . 3 |- (ph -> (ps -> ch))
3		bitrd.2	. . 3 |- (ph -> (ch <-> th))
4	2, 3	sylibd 200	. 2 |- (ph -> (ps -> th))
5	3	biimprd 152	. . 3 |- (ph -> (th -> ch))
6	5, 1	sylibrd 202	. 2 |- (ph -> (th -> ps))
7	4, 6	impbid 519	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  bitr2d 532  bitr3d 533  bitr4d 534  syl5bb 535  syl6bb 539  sylan9bb 543  3bitrd 547  3bitr2d 549  3bitr3d 551  3bitr4d 553  bibi2d 621  imbi12d 629  orbi12d 630  anbi12d 631  bibi12d 632  dedlem0a 765  dedlema 767  ax11el 1403  eqeq12d 1532  eleq12d 1585  raleqd 1837  rexeqd 1838  reueqd 1839  raleq12d 1840  rexeq12d 1841  sbc8g 2004  elrabsf 2011  sbcth2 2030  hbsbcgd 2032  sbc19.21g 2035  sbcralt 2040  sbcrext 2041  sbcralgf 2042  sbcrexgf 2043  sbcabel 2046  ra4sbc 2047  csbcog 2058  sbcel12g 2062  sbcel1g 2064  sbceq1dig 2065  sbcel2g 2066  sbceq2dig 2067  sbcco3g 2093  sseq12d 2142  psseq12d 2194  raaan 2414  dedth2vOLD 2438  dedth4vOLD 2440  elimhyp2v 2448  elimhyp4v 2450  keephyp2v 2454  breq12d 2704  hbbrd 2732  sbcbrg 2736  sbcbr12g 2737  sbcbr1g 2738  sbcbr2g 2739  csbopabg 2752  treq 2760  nalset 2786  copsex4g 2870  opelopab2 2896  posn 2928  efrirr 2957  limeq 2987  ordtri1 3008  elpwun 3134  ordpwsuc 3172  ordunisuc2 3198  tfindsg 3213  dfom2 3220  findsg 3245  vtoclrbr 3295  vtoclibr 3296  ididg 3368  fconst 3765  fnrnfv 3870  dmfco 3884  fvopabn 3897  funimass3 3920  funconstss 3922  dffo3 3933  fressnfv 3952  f1ofveu 3996  isomin 4013  isoini 4014  isowe 4017  f1oiso 4018  f1oweALT 4020  oprabval 4083  dfopab2 4173  dfoprab3 4174  fparlem1 4199  fparlem2 4200  oe0m1 4296  oaord1 4321  omord 4335  omlimcl 4345  oewordi 4354  nnaordr 4376  nnaordex 4389  nnawordex 4390  ereq 4407  erref 4415  brecop 4447  eceqopreq 4454  elmapg 4474  dom2d 4545  sbthlem2 4593  sbth 4602  nndomo 4667  unfilem2 4695  unfilem3 4696  elirr 4742  infeq5 4766  r1pw 4832  rankxplim 4858  aceq6b 4888  kmlem2 4912  brdom7disj 4950  brdom6disj 4951  unidom 4954  iscard2 5004  axpownd 5107  ltapi 5184  ltmpi 5185  nlt1pi 5187  indpi 5188  enqeceq 5201  ltapq 5230  genpass 5266  mulclprlem 5275  distrlem1pr 5281  distrlem5pr 5285  1idpr 5287  prlem936b 5308  prlem936 5309  reclem4pr 5313  enreceq 5331  addgt0sr 5367  sqgt0sr 5369  ltresr 5412  cnegexlem1 5499  ltxr 5649  ltxrlt 5654  leloe 5672  eqlelt 5673  xrleloe 5711  ltadd2 5778  leadd2 5780  ltaddsub2 5786  leaddsub2 5788  ltaddpos 5805  ltnegcon1 5810  lenegcon1 5812  lenegcon2 5813  lesub1 5814  ltsub1 5816  addge01 5826  addge02 5827  mulcan2 5845  ltmuldivi 5965  ltmul2 5971  ltmul2OLD 5972  lemul2 5975  lemul2OLD 5976  ltmulgt11 5990  ltmulgt12 5991  gt0div 5997  ge0div 5998  ledivmul2OLD 6019  ltdiv2 6032  ltrec1 6033  lerec2 6034  ledivdiv 6035  ltdiv23 6037  lediv23 6038  nnleltp1 6100  rpneg 6211  nnrecl 6240  supxrre2 6262  nn0sub 6329  znnsub 6345  zltp1le 6349  btwnnz 6363  gtndiv 6364  uzindOLD 6379  uzwo4OLD 6381  flval3 6438  btwnzge0 6445  ioo0 6494  elioo3g 6506  icoshftf1olem 6537  icounlem 6539  eluz2 6548  uzwo 6582  uzwoOLD 6583  elfz2 6600  fzen 6622  fzsubel 6631  fzrevral2 6651  fzrevral3 6652  fzshftral 6653  expeq0 6780  sq01 6848  absrpcl 7057  sqabs 7071  absdiflt 7086  absdifle 7087  lenegsq 7088  dffsum 7201  fsum1s2 7213  clm0i 7286  clm0nnsi 7288  climshft2i 7309  caucvgi 7366  dfisum 7395  efcltlem1 7509  reeff1o 7634  efieq 7658  nn0ennn 7709  infxpidmlem2 7765  infxpidmlem3 7766  infxpidmlem11 7774  eltg 7830  eltg2 7831  iscld 7879  iscld4 7906  elcls2 7915  elcls3 7921  isnei 7928  islp2 7957  cldlp 7960  iscn 7968  iscnp 7970  iscnp2 7971  iscncl 7980  cncnp2 7989  sncld 7997  ismet 8008  metn0 8031  metreslem 8032  metxp 8044  elbl3 8050  blrn 8051  isopn 8069  isopn4 8072  metcnplem 8097  metcnp 8098  metcnp2 8099  metcn 8100  metcnp3 8107  cncfmet 8116  bl2ioo 8122  ioo2bl 8123  lmbrf 8141  iscau 8147  iscau5 8152  iscaunns 8155  lmclim 8174  metcnp4 8181  metcn4 8182  cncms 8209  bcthlem1 8210  bcthlem25 8234  isgrp 8254  grplactf1o 8339  isabl 8342  isring 8382  ringi 8383  vci 8414  isvclem 8443  vcoprnelem 8444  nvsubadd 8522  nvelbl 8572  nvelbl2 8573  nmo0 8706  blocnilem 8719  isph 8737  pilem3 8940  sincosq2sgn 8972  sinq12gt0t 8975  efifolem6 8999  efifolem7 9000  eff1i 9016  logltb 9048  h2hlm 9125  hvaddeq0 9211  hial2eq2 9249  norm-i 9272  hhcms 9348  hhssnv 9410  hhsscms 9426  projlem2 9463  pjeq 9518  shsel3 9555  chssoc 9695  chsscon1 9700  chsscon2 9701  chpsscon1 9703  chpsscon2 9704  chlejb2 9712  elspansn2 9766  fh1 9837  fh2 9838  cm2j 9839  eigposi 10042  unopf1o 10120  nmcopexlem3 10232  lnopcnre 10247  nmcfnexlem3 10261  riesz4i 10275  leop2 10337  leop3 10338  leoppos 10339  hst1h 10435  mdbr2 10504  mdbr3 10505  mdbr4 10506  dmdbr2 10511  dmdbr3 10513  dmdbr4 10514  mddmd2 10517  cvdmd 10545  atcvatlem 10594  atdmd 10607  sumdmdii 10624  dmdbr5ati 10631  cdj3lem1 10643  elghomlem2 10668  symgval 10688  nndivlub 10707  elo 10733  feq123 10774  islatalg 10831  sppfi 10851  istoset 10861  isass 10890  ismgm 10897  opidon2 10900  ismnd1 10927  grpmnd 10933  iscom2 10940  zrdivrng 10969  cdrci 10994  islp3 11011  ishomeo 11023  issubsp 11057  cnfilca 11088  iintlem1 11155  ismgra 11164  isalg 11175  algi 11181  ismonb 11265  ismonc 11269  isepib 11275  iepiclem 11278  isepic 11279  isfunb 11289  issubcata 11300  elicc3 11410  ccid 11412  elfiun 11421  hausnei2 11471  subspid 11478  compsub 11488  hscptsscld 11491  reconnlem5 11511  ivthALT 11515  2ndcsb 11537  isfne3 11543  topbasfne 11560  topfneec 11562  neibastop2lem4 11583  ist1-2 11603  ist1-3 11604  isnrm2 11613  fbunfip 11631  elfg 11633  neifg 11644  ufileu 11658  filufint 11659  flimopn 11679  fbaslim 11680  limfilcf 11683  hausfillim 11685  cnpfillim 11686  elfilmap2 11691  elfilmap3 11692  isflimf 11709  flimfcnp 11714  flimfcn 11715  isfclus 11718  fclusnei 11719  flimfcls 11725  fcluscn 11731  ufcomp 11734  fclusfnei 11738  fclsfcn 11744  eltail 11758  isga 11772  f1elima 11818  upixp 11823  dif1en 11833  acdcg 11842  acdc3g 11843  acdc5g 11844  fzpr 11866  mod0 11871  negmod0 11872  sdclem1 11875  sdclem2 11876  sdc 11877  metsstop 11909  mettrifi2 11913  hmeocld 11961  tlmbrf 11966  lmtlm 11969  tx1cn 11976  tx2cn 11977  uptx 11978  txsubsp 11983  isismty 12004  ismtyhmeolem 12006  ismtyhmeo 12007  ismtyres 12010  heiborlem36 12046  bfp 12065  rrnmet 12072  rrnheibor 12079  isphtpc 12101  hgrablkcard 12200

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 145  df-an 223

Copyright terms: Public domain