Theorem bitr3d 529

Description: Deduction form of bitr3 175.

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 520	. 2 |- (ph -> (ch <-> ps))
3		bitr3d.2	. 2 |- (ph -> (ps <-> th))
4	2, 3	bitrd 527	1 |- (ph -> (ch <-> th))

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

This theorem is referenced by:  3bitrrd 544  3bitr3d 547  3bitr3rd 548  biass 743  19.23t 1114  sbequ12a 1181  sbco2 1253  sbco3 1255  sbcom 1256  sb9i 1261  sbcom2 1332  sbal1 1344  sbal 1345  elabf 1892  sbcel1gv 1976  sbcel2gv 1977  sbcgf 1982  sbccomg 1985  sbccsbg 2018  iununi 2611  copsex2g 2788  opabsb 2810  ordtri2 2977  onmindif 3055  onmindif2 3056  ordunisuc2 3110  dfom2 3128  fnssresb 3591  fcnvres 3639  fvopab5 3784  funimass5 3798  isocnv 3887  isoini 3891  ordge1n0 4135  oa00 4183  odi 4200  mapxpen 4481  omsucdom 4508  isfinite2 4529  unfilem1 4530  fodomfib 4547  rankr1a 4657  bnd2 4704  fodomb 4780  domtri 4818  iscard 4833  suplem2pr 5142  cnegextlem3 5327  addcan2t 5333  subcan2t 5382  subeq0t 5383  negcon1t 5390  lesubt 5618  ltsub13t 5624  diveq0t 5732  ltmuldiv2t 5826  lemuldiv2t 5833  lt2msq 5837  nn1suc 5895  nnsub 5911  avglet 5999  supxrre 6038  supxrbnd 6046  elnn0nn 6126  elnnnn0 6127  znn0subt 6133  primet 6150  dfuz 6158  uzindOLD 6164  zbtwnre 6177  om2uzlt2 6244  fznt 6433  fzrev3t 6454  sqrmsq2 6644  absdifltt 6829  absdiflet 6830  expcnvlem6 7175  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  sinbndt 7415  cosbndt 7416  znnen 7453  unbenlem 7455  eltopt 7579  eltop2t 7580  eltop3t 7581  bcthlem18 7966  grpid 8015  nvsubadd 8227  nvmeq0 8236  nvgt0 8255  imsmetlem 8274  nmlnogt0 8402  ip2eqi 8461  eff1i 8683  logeftb 8703  h2hcau 8788  h2hlm 8789  hvaddcan2t 8877  hvmulcant 8878  hvaddsub4t 8884  hi2eqt 8910  hcau2 8994  lnopeq 9871  riesz1t 9936  jp 10135  chcv2t 10220  cvp 10239  atnem0 10241  cdj3lem1 10295  ghomf1olem 10330  cnfilca 10487

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