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

Theorem bitr4d 184
Description: Deduction form of bitr4i 180. (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 133 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 181 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3bitr2d  209  3bitr2rd  210  3bitr4d  213  3bitr4rd  214  bianabs  553  imordc  807  3anibar  1083  xor2dc  1297  bilukdc  1303  reuhypd  4231  opelresi  4651  iota1  4909  funbrfv2b  5246  dffn5im  5247  fneqeql  5303  f1ompt  5348  dff13  5435  fliftcnv  5463  isotr  5484  isoini  5485  caovord3  5702  releldm2  5839  tpostpos  5910  nnaordi  6112  iserd  6163  ecdmn0m  6179  qliftel  6217  qliftfun  6219  qliftf  6222  ecopovsym  6233  supisolem  6412  recmulnqg  6547  nqtri3or  6552  ltmnqg  6557  mullocprlem  6726  addextpr  6777  gt0srpr  6891  ltsosr  6907  ltasrg  6913  xrlenlt  7143  letri3  7158  subadd  7277  ltsubadd2  7502  lesubadd2  7504  suble  7509  ltsub23  7511  ltaddpos2  7522  ltsubpos  7523  subge02  7547  ltaddsublt  7636  reapneg  7662  apsym  7671  apti  7687  leltap  7689  ap0gt0  7703  divmulap  7728  divmulap3  7730  rec11rap  7762  ltdiv1  7909  ltdivmul2  7919  ledivmul2  7921  ltrec  7924  nnle1eq1  8014  avgle1  8222  avgle2  8223  nn0le0eq0  8267  znnnlt1  8350  zleltp1  8357  elz2  8370  uzm1  8599  uzin  8601  difrp  8717  xrletri3  8822  xltnegi  8849  elioo5  8903  elfz5  8984  fzdifsuc  9045  elfzm11  9055  uzsplit  9056  elfzonelfzo  9188  qtri3or  9200  qavgle  9215  flqbi  9240  flqbi2  9241  zmodid2  9302  q2submod  9335  sqap0  9486  lt2sq  9493  le2sq  9494  nn0opthlem1d  9588  ibcval5  9631  shftfib  9652  mulreap  9692  caucvgrelemcau  9807  caucvgre  9808  elicc4abs  9921  abs2difabs  9935  cau4  9943  clim2  10035  climeq  10051  dvdsval3  10112  dvdslelemd  10155  dvdsabseq  10159  dvdsflip  10163  dvdsssfz1  10164  zeo3  10179  ndvdsadd  10243  algcvgblem  10271
  Copyright terms: Public domain W3C validator