ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitr3d Unicode version

Theorem bitr3d 189
Description: Deduction form of bitr3i 185. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
Assertion
Ref Expression
bitr3d  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bicomd 140 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 187 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3bitrrd  214  3bitr3d  217  3bitr3rd  218  pm5.16  798  biassdc  1358  pm5.24dc  1361  anxordi  1363  sbequ12a  1731  drex1  1754  sbcomxyyz  1923  sb9v  1931  csbiebt  3009  prsspwg  3649  bnd2  4067  copsex2t  4137  copsex2g  4138  fnssresb  5205  fcnvres  5276  dmfco  5457  funimass5  5505  fmptco  5554  cbvfo  5654  cbvexfo  5655  isocnv  5680  isoini  5687  isoselem  5689  riota2df  5718  ovmpodxf  5864  caovcanrd  5902  fidcenumlemrks  6809  ordiso2  6888  ltpiord  7095  dfplpq2  7130  dfmpq2  7131  enqeceq  7135  enq0eceq  7213  enreceq  7512  ltpsrprg  7579  mappsrprg  7580  cnegexlem3  7907  subeq0  7956  negcon1  7982  subexsub  8102  subeqrev  8106  lesub  8171  ltsub13  8173  subge0  8205  div11ap  8427  divmuleqap  8444  ltmuldiv2  8597  lemuldiv2  8604  nn1suc  8703  addltmul  8914  elnnnn0  8978  znn0sub  9077  prime  9108  indstr  9344  qapne  9387  qlttri2  9389  fz1n  9779  fzrev3  9822  fzonlt0  9899  divfl0  10024  modqsubdir  10121  fzfig  10158  sqrt11  10766  sqrtsq2  10770  absdiflt  10819  absdifle  10820  nnabscl  10827  minclpr  10963  xrnegiso  10986  xrnegcon1d  10988  clim2  11007  climshft2  11030  sumrbdc  11102  sinbnd  11373  cosbnd  11374  dvdscmulr  11434  dvdsmulcr  11435  oddm1even  11484  qredeq  11689  cncongr2  11697  isprm3  11711  prmrp  11735  sqrt2irr  11752  crth  11811  eltg3  12137  eltop  12149  eltop2  12150  eltop3  12151  lmbrf  12295  cncnpi  12308  txcn  12355  hmeoimaf1o  12394  ismet2  12434  xmseq0  12548
  Copyright terms: Public domain W3C validator