Theorem bitr3d 533

Description: Deduction form of bitr3i 173.

Hypotheses

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

Assertion

Ref	Expression
bitr3d	|- (ph -> (ch <-> th))

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bicomd 524	. 2 |- (ph -> (ch <-> ps))
3		bitr3d.2	. 2 |- (ph -> (ps <-> th))
4	2, 3	bitrd 531	1 |- (ph -> (ch <-> th))

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

This theorem is referenced by:  3bitrrd 548  3bitr3d 551  3bitr3rd 552  biass 749  19.23t 1152  sbequ12a 1220  sbco2 1293  sbco3 1295  sbcom 1296  sb9i 1301  sbcom2 1373  sbal1 1385  sbal 1386  elabf 1942  sbc7g 2003  sbcel1gv 2028  sbcel2gv 2029  sbcgf 2034  sbccomg 2039  sbccsbg 2073  iununi 2686  copsex2g 2869  opelopabsb 2892  ordtri2 3010  onmindif 3061  onmindif2 3169  ordunisuc2 3198  dfom2 3220  fnssresb 3705  fcnvres 3755  fvopab5 3904  funimass5 3921  isocnv 4010  isoini 4014  ordge1n0 4281  oa00 4329  odi 4346  oeoe 4362  mapxpen 4642  omsucdom 4669  isfinite2 4692  unfilem1 4694  fodomfib 4710  rankr1a 4823  bnd2 4870  fodomb 4946  domtri 4987  iscard 5003  suplem2pr 5316  cnegexlem3 5501  addcan2 5507  subcan2 5556  subeq0 5557  negcon1 5564  lesub 5790  ltsub13 5796  diveq0 5907  ltmuldiv2 6009  ltmuldiv2OLD 6010  lemuldiv2 6021  lemuldiv2OLD 6022  lt2msqi 6026  nn1suc 6084  nnsubi 6102  avgle 6190  supxrre 6251  supxrbnd 6259  elnn0nn 6339  elnnnn0 6340  znn0sub 6346  prime 6366  dfuzi 6373  uzindOLD 6379  zbtwnre 6393  modsubdir 6480  fzn 6621  fzrev3 6645  om2uzlt2i 6662  sqrmsq2i 6907  absdiflt 7086  absdifle 7087  expcnvlem6 7436  mulc1cncf 7484  ivthlem6 7491  ivthlem7 7492  sinbnd 7674  cosbnd 7675  znnen 7714  unbenlem 7716  eltop 7841  eltop2 7842  eltop3 7843  bcthlem18 8227  grpid 8282  nvsubadd 8522  nvmeq0 8531  nvgt0 8550  imsmetlem 8570  nmlnogt0 8712  ip2eqi 8773  eff1i 9016  logeftb 9036  h2hcau 9124  h2hlm 9125  hvaddcan2 9213  hvmulcanOLD 9215  hvmulcan2 9216  hvaddsub4 9221  hi2eq 9247  hcau2 9331  lnopeqi 10212  riesz1 10277  jpi 10478  chcv2 10564  cvp 10583  atnem0 10585  atnem0OLD 10586  cdj3lem1 10643  ghomf1olem 10681  cnfilca 11088  ordiso 11426  topfne 11561  flimopn 11679  geomcau 11914  recms 12066

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