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

Theorem bitr4d 190
Description: Deduction form of bitr4i 186. (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 140 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 187 1  |-  ( ph  ->  ( ps  <->  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:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  435  mpbiran2d  436  bianabs  583  imordc  865  3anibar  1132  xor2dc  1351  bilukdc  1357  reuhypd  4360  opelresi  4798  iota1  5070  funbrfv2b  5432  dffn5im  5433  fneqeql  5494  f1ompt  5537  dff13  5635  fliftcnv  5662  isotr  5683  isoini  5685  caovord3  5910  releldm2  6049  tpostpos  6127  nnsssuc  6364  nnaordi  6370  iserd  6421  ecdmn0m  6437  qliftel  6475  qliftfun  6477  qliftf  6480  ecopovsym  6491  mapen  6706  supisolem  6861  cnvti  6872  omp1eomlem  6945  ctssdc  6964  isomnimap  6975  ismkvmap  6994  recmulnqg  7163  nqtri3or  7168  ltmnqg  7173  mullocprlem  7342  addextpr  7393  gt0srpr  7520  ltsosr  7536  ltasrg  7542  map2psrprg  7577  xrlenlt  7793  letri3  7809  subadd  7929  ltsubadd2  8159  lesubadd2  8161  suble  8166  ltsub23  8168  ltaddpos2  8179  ltsubpos  8180  subge02  8204  ltaddsublt  8296  reapneg  8322  apsym  8331  apti  8347  leltap  8350  ap0gt0  8364  divmulap  8395  divmulap3  8397  rec11rap  8431  ltdiv1  8583  ltdivmul2  8593  ledivmul2  8595  ltrec  8598  suprleubex  8669  nnle1eq1  8701  avgle1  8911  avgle2  8912  nn0le0eq0  8956  znnnlt1  9053  zleltp1  9060  elz2  9073  uzm1  9305  uzin  9307  difrp  9426  xrletri3  9528  xgepnf  9539  xltnegi  9558  xltadd1  9599  xposdif  9605  xleaddadd  9610  elioo5  9656  elfz5  9738  fzdifsuc  9801  elfzm11  9811  uzsplit  9812  elfzonelfzo  9947  qtri3or  9960  qavgle  9976  flqbi  10003  flqbi2  10004  zmodid2  10065  q2submod  10098  sqap0  10299  lt2sq  10306  le2sq  10307  nn0opthlem1d  10406  bcval5  10449  zfz1isolemiso  10522  shftfib  10535  mulreap  10576  caucvgrelemcau  10692  caucvgre  10693  elicc4abs  10806  abs2difabs  10820  cau4  10828  maxclpr  10934  negfi  10939  lemininf  10945  mul0inf  10952  xrlemininf  10980  xrminltinf  10981  clim2  10992  climeq  11008  fisumss  11101  fsumabs  11174  isumshft  11199  absefib  11375  dvdsval3  11393  dvdslelemd  11437  dvdsabseq  11441  dvdsflip  11445  dvdsssfz1  11446  zeo3  11461  ndvdsadd  11524  dvdssq  11615  algcvgblem  11626  lcmdvds  11656  ncoprmgcdgt1b  11667  isprm3  11695  phiprmpw  11793  discld  12200  isneip  12210  restopnb  12245  restopn2  12247  restdis  12248  lmbr2  12278  cnptoprest  12303  cnptoprest2  12304  tx1cn  12333  tx2cn  12334  txcnmpt  12337  txrest  12340  elbl2ps  12456  elbl2  12457  blcomps  12460  blcom  12461  xblpnfps  12462  xblpnf  12463  blpnf  12464  xmeter  12500  bdxmet  12565  metrest  12570  xmetxp  12571  metcn  12578  cncffvrn  12633
  Copyright terms: Public domain W3C validator