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

Theorem bitr3d 188
Description: Deduction form of bitr3i 184. (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 139 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 186 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitrrd  213  3bitr3d  216  3bitr3rd  217  pm5.16  771  biassdc  1327  pm5.24dc  1330  anxordi  1332  sbequ12a  1697  drex1  1720  sbcomxyyz  1888  sb9v  1896  csbiebt  2943  prsspwg  3552  bnd2  3955  copsex2t  4008  copsex2g  4009  fnssresb  5042  fcnvres  5104  dmfco  5273  funimass5  5316  fmptco  5362  cbvfo  5456  cbvexfo  5457  isocnv  5482  isoini  5488  isoselem  5490  riota2df  5519  ovmpt2dxf  5657  caovcanrd  5695  ordiso2  6505  ltpiord  6571  dfplpq2  6606  dfmpq2  6607  enqeceq  6611  enq0eceq  6689  enreceq  6975  cnegexlem3  7352  subeq0  7401  negcon1  7427  subexsub  7543  subeqrev  7547  lesub  7612  ltsub13  7614  subge0  7646  div11ap  7855  divmuleqap  7872  ltmuldiv2  8020  lemuldiv2  8027  nn1suc  8125  addltmul  8334  elnnnn0  8398  znn0sub  8497  prime  8527  indstr  8762  qapne  8805  qlttri2  8807  fz1n  9139  fzrev3  9180  fzonlt0  9253  divfl0  9378  modqsubdir  9475  fzfig  9512  sqrt11  10063  sqrtsq2  10067  absdiflt  10116  absdifle  10117  nnabscl  10124  clim2  10260  climshft2  10283  isumrb  10339  dvdscmulr  10369  dvdsmulcr  10370  oddm1even  10419  qredeq  10622  cncongr2  10630  isprm3  10644  prmrp  10668  sqrt2irr  10685
  Copyright terms: Public domain W3C validator