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

Theorem bitrd 181
Description: Deduction form of bitri 177. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
Hypotheses
Ref Expression
bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
Assertion
Ref Expression
bitrd  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem bitrd
StepHypRef Expression
1 bitrd.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.74i 173 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 173 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 177 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 174 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:  bitr2d  182  bitr3d  183  bitr4d  184  syl5bb  185  syl6bb  189  3bitrd  207  3bitr2d  209  3bitr3d  211  3bitr4d  213  imbi12d  227  bibi12d  228  sylan9bb  443  anbi12d  450  orbi12d  717  con1biidc  782  pm4.54dc  816  dn1dc  878  dedlem0a  886  xorbi12d  1289  nbbndc  1301  eleq12d  2124  neeq12d  2240  neleq12d  2320  raleqbi1dv  2530  rexeqbi1dv  2531  reueqd  2532  rmoeqd  2533  raleqbidv  2534  rexeqbidv  2535  raleqbidva  2536  rexeqbidva  2537  eueq3dc  2738  sbc19.21g  2854  sbcabel  2867  sbcel1g  2897  sbceq1g  2898  sbcel2g  2899  sbceq2g  2900  sbccsb2g  2907  sbcco3g  2931  sseq12d  3002  psseq12d  3066  raaanlem  3354  sbcssg  3358  ralsng  3439  rexsng  3440  2ralunsn  3597  csbunig  3616  disjeq12d  3782  breq123d  3806  sbcbr12g  3842  sbcbr1g  3843  sbcbr2g  3844  treq  3888  nalset  3915  copsex4g  4012  sucelon  4257  posng  4440  csbxpg  4449  sbcrel  4454  csbcnvg  4547  eliniseg  4723  brcodir  4740  csbrng  4810  sbcfung  4953  fneq12d  5019  feq12d  5064  feq123d  5065  sbcfng  5072  sbcfg  5073  f1osng  5195  csbfv12g  5237  funimass4  5252  dmfco  5269  eqfnfv  5293  eqfnfv2  5294  fneqeql2  5304  fvimacnvi  5309  funimass3  5311  fniniseg  5315  rexsupp  5319  unpreima  5320  ralrnmpt  5337  rexrnmpt  5338  dffo3  5342  fmptco  5358  fressnfv  5378  eufnfv  5417  fnunirn  5434  dff13  5435  f1elima  5440  cocan1  5455  cocan2  5456  fliftel  5461  fliftf  5467  isoresbr  5477  isoini  5485  f1oiso  5493  f1ofveu  5528  mpt2eq123dva  5594  ovid  5645  ov  5648  ovg  5667  ovelrn  5677  caovord2d  5698  ofrfval2  5755  offveqb  5758  eqop  5831  reldm  5840  f1od2  5884  mpt2xopoveq  5886  mpt2xopovel  5887  isprmpt2  5889  tpostpos  5910  smoiso  5948  frecsuclem3  6021  nnaordr  6114  nnaword  6115  nnaordex  6131  ereq1  6144  brdifun  6164  erth2  6182  qliftfun  6219  brecop  6227  dom2lem  6283  xpcomco  6331  php5fin  6370  supisolem  6412  ltapig  6494  ltmpig  6495  nlt1pig  6497  mulcmpblnq  6524  ltsonq  6554  lt2addnq  6560  lt2mulnq  6561  archnqq  6573  prarloclemarch  6574  ltrnqg  6576  mulcmpblnq0  6600  preqlu  6628  genpdflem  6663  addnqprllem  6683  addnqprulem  6684  addlocprlemgt  6690  appdivnq  6719  mulnqprl  6724  mulnqpru  6725  mullocprlem  6726  distrlem4prl  6740  distrlem4pru  6741  1idprl  6746  1idpru  6747  ltexprlemloc  6763  cauappcvgprlemladdrl  6813  cauappcvgprlemladd  6814  cauappcvgprlem1  6815  archrecnq  6819  caucvgprlemnkj  6822  caucvgprprlemexb  6863  addcmpblnr  6882  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1  6923  srpospr  6925  caucvgsrlemcau  6935  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  ltresr  6973  axcaucvglemres  7031  cnegexlem1  7249  negeu  7265  subadd2  7278  subcan2  7299  addrsub  7441  ltaddneg  7493  ltaddnegr  7494  ltadd1  7498  leadd2  7500  ltsubadd  7501  lesubadd  7503  ltaddsub2  7506  leaddsub2  7508  ltaddpos  7521  lesub2  7526  ltsub2  7528  ltnegcon1  7532  ltnegcon2  7533  lenegcon1  7535  lenegcon2  7536  addge01  7541  addge02  7542  suble0  7545  leaddle0  7546  lesub0  7548  sublt0d  7635  recexre  7643  reaplt  7653  reapltxor  7654  reapneg  7662  remulext1  7664  apreim  7668  apcotr  7672  apadd2  7674  addext  7675  mulcanap2d  7717  diveqap0  7735  diveqap1  7756  ltmul2  7897  lemul2  7898  ltmulgt11  7905  ltmulgt12  7906  gt0div  7911  ge0div  7912  ltmuldiv  7915  ltrec1  7929  lerec2  7930  ledivdiv  7931  ltdiv23  7933  lediv23  7934  creur  7987  creui  7988  nn1suc  8009  nnrecl  8237  znnsub  8353  zgt0ge1  8360  zltlen  8377  nn0n0n1ge2b  8378  btwnnz  8392  gtndiv  8393  prime  8396  eluz2  8575  indstr2  8643  negm  8647  nn01to3  8649  qapne  8671  qltlen  8672  qreccl  8674  divlt1lt  8748  divle1le  8749  nnledivrp  8784  iccid  8895  elioc2  8906  elico2  8907  elicc2  8908  elfz2  8983  fzen  9009  fzsubel  9025  elfzp1  9036  fzpr  9041  fzrevral2  9070  fzrevral3  9071  nn0disj  9097  2ffzeq  9100  fzosplitsni  9193  fvinim0ffz  9198  ioo0  9216  ico0  9218  ioc0  9219  modq0  9279  negqmod0  9281  zmodidfzo  9303  frecuzrdgfn  9362  nn0ennn  9373  sq11  9492  nn0le2msqd  9587  nn0opth2d  9591  2shfti  9660  cjap  9734  rexfiuz  9816  rexanuz2  9818  abs00ap  9889  absext  9890  sqabs  9909  abslt  9915  absle  9916  absdiflt  9919  absdifle  9920  lenegsq  9922  clim  10033  clim0c  10038  climrecvg1n  10098  dvdsval2  10111  modmulconst  10139  dvdsaddr  10151  dvdsabseq  10159  fzocongeq  10170  zeo3  10179  odd2np1  10184  oddp1d2  10202  zob  10203  oddm1d2  10204  nnoddm1d2  10222  divalgb  10237  divalgmod  10239  modremain  10241  oddpwdclemxy  10257  oddpwdclemodd  10260  nn0seqcvgd  10263  algcvgblem  10271  cbvrald  10314  bj-nalset  10402  bj-sels  10421  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator