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

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

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bitr4d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32bicomd 139 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 186 1  |-  ( ph  ->  ( ps  <->  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:  3bitr2d  214  3bitr2rd  215  3bitr4d  218  3bitr4rd  219  bianabs  578  imordc  834  3anibar  1111  xor2dc  1326  bilukdc  1332  reuhypd  4284  opelresi  4712  iota1  4981  funbrfv2b  5333  dffn5im  5334  fneqeql  5391  f1ompt  5434  dff13  5529  fliftcnv  5556  isotr  5577  isoini  5579  caovord3  5800  releldm2  5937  tpostpos  6011  nnaordi  6247  iserd  6298  ecdmn0m  6314  qliftel  6352  qliftfun  6354  qliftf  6357  ecopovsym  6368  mapen  6542  supisolem  6682  cnvti  6693  isomnimap  6772  recmulnqg  6929  nqtri3or  6934  ltmnqg  6939  mullocprlem  7108  addextpr  7159  gt0srpr  7273  ltsosr  7289  ltasrg  7295  xrlenlt  7530  letri3  7545  subadd  7664  ltsubadd2  7890  lesubadd2  7892  suble  7897  ltsub23  7899  ltaddpos2  7910  ltsubpos  7911  subge02  7935  ltaddsublt  8024  reapneg  8050  apsym  8059  apti  8075  leltap  8077  ap0gt0  8091  divmulap  8116  divmulap3  8118  rec11rap  8152  ltdiv1  8301  ltdivmul2  8311  ledivmul2  8313  ltrec  8316  suprleubex  8387  nnle1eq1  8418  avgle1  8626  avgle2  8627  nn0le0eq0  8671  znnnlt1  8768  zleltp1  8775  elz2  8788  uzm1  9018  uzin  9020  difrp  9139  xrletri3  9239  xltnegi  9266  elioo5  9320  elfz5  9401  fzdifsuc  9462  elfzm11  9472  uzsplit  9473  elfzonelfzo  9606  qtri3or  9619  qavgle  9635  flqbi  9662  flqbi2  9663  zmodid2  9724  q2submod  9757  sqap0  9986  lt2sq  9993  le2sq  9994  nn0opthlem1d  10093  ibcval5  10136  zfz1isolemiso  10209  shftfib  10222  mulreap  10263  caucvgrelemcau  10378  caucvgre  10379  elicc4abs  10492  abs2difabs  10506  cau4  10514  maxclpr  10620  negfi  10623  lemininf  10628  clim2  10635  climeq  10651  fisumss  10748  fsumabs  10822  isumshft  10846  dvdsval3  10893  dvdslelemd  10937  dvdsabseq  10941  dvdsflip  10945  dvdsssfz1  10946  zeo3  10961  ndvdsadd  11024  dvdssq  11113  algcvgblem  11124  lcmdvds  11154  ncoprmgcdgt1b  11165  isprm3  11193  phiprmpw  11291
  Copyright terms: Public domain W3C validator