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

Theorem bitrd 187
Description: Deduction form of bitri 183. (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 179 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 179 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 183 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 180 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:  bitr2d  188  bitr3d  189  bitr4d  190  syl5bb  191  syl6bb  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  457  anbi12d  464  orbi12d  767  con1biidc  847  pm4.54dc  872  dn1dc  929  dedlem0a  937  xorbi12d  1345  nbbndc  1357  eleq12d  2188  neeq12d  2305  neleq12d  2386  raleqbi1dv  2611  rexeqbi1dv  2612  reueqd  2613  rmoeqd  2614  raleqbidv  2615  rexeqbidv  2616  raleqbidva  2617  rexeqbidva  2618  eueq3dc  2831  sbc19.21g  2949  sbcabel  2962  sbcel1g  2992  sbceq1g  2993  sbcel2g  2994  sbceq2g  2995  sbccsb2g  3002  sbcco3g  3027  sseq12d  3098  raaanlem  3438  sbcssg  3442  ralsng  3534  2ralunsn  3695  csbunig  3714  disjeq12d  3885  breq123d  3913  sbcbr12g  3953  sbcbr1g  3954  sbcbr2g  3955  treq  4002  nalset  4028  exmidsssn  4095  copsex4g  4139  sucelon  4389  posng  4581  csbxpg  4590  sbcrel  4595  csbcnvg  4693  eliniseg  4879  brcodir  4896  csbrng  4970  sbcfung  5117  fneq12d  5185  feq12d  5232  feq123d  5233  sbcfng  5240  sbcfg  5241  f1osng  5376  csbfv12g  5425  funimass4  5440  dmfco  5457  eqfnfv  5486  eqfnfv2  5487  fneqeql2  5497  fvimacnvi  5502  funimass3  5504  fniniseg  5508  rexsupp  5512  unpreima  5513  ralrnmpt  5530  rexrnmpt  5531  dffo3  5535  fmptco  5554  fressnfv  5575  eufnfv  5616  foima2  5621  fnunirn  5636  dff13  5637  f1elima  5642  cocan1  5656  cocan2  5657  fliftel  5662  fliftf  5668  isoresbr  5678  isoini  5687  f1oiso  5695  f1ofveu  5730  mpoeq123dva  5800  ovid  5855  ov  5858  ovg  5877  ovelrn  5887  caovord2d  5908  ofrfval2  5966  offveqb  5969  eqop  6043  reldm  6052  f1od2  6100  mpoxopoveq  6105  mpoxopovel  6106  tpostpos  6129  smoiso  6167  frecabcl  6264  frecsuclem  6271  nnaordr  6374  nnaword  6375  nnaordex  6391  ereq1  6404  brdifun  6424  erth2  6442  qliftfun  6479  brecop  6487  elmapg  6523  elpmg  6526  dom2lem  6634  xpcomco  6688  php5fin  6744  elfi2  6828  supisolem  6863  inflbti  6879  inl11  6918  ismkvnex  6997  mkvprop  7000  exmidfodomrlemreseldju  7024  ltapig  7114  ltmpig  7115  nlt1pig  7117  mulcmpblnq  7144  ltsonq  7174  lt2addnq  7180  lt2mulnq  7181  archnqq  7193  prarloclemarch  7194  ltrnqg  7196  mulcmpblnq0  7220  preqlu  7248  genpdflem  7283  addnqprllem  7303  addnqprulem  7304  addlocprlemgt  7310  appdivnq  7339  mulnqprl  7344  mulnqpru  7345  mullocprlem  7346  distrlem4prl  7360  distrlem4pru  7361  1idprl  7366  1idpru  7367  ltexprlemloc  7383  cauappcvgprlemladdrl  7433  cauappcvgprlemladd  7434  cauappcvgprlem1  7435  archrecnq  7439  caucvgprlemnkj  7442  caucvgprprlemexb  7483  addcmpblnr  7515  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1  7557  srpospr  7559  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  map2psrprg  7581  ltresr  7615  axcaucvglemres  7675  cnegexlem1  7905  negeu  7921  subadd2  7934  subcan2  7955  addrsub  8101  ltaddneg  8154  ltaddnegr  8155  ltadd1  8159  leadd2  8161  ltsubadd  8162  lesubadd  8164  ltaddsub2  8167  leaddsub2  8169  ltaddpos  8182  lesub2  8187  ltsub2  8189  ltnegcon1  8193  ltnegcon2  8194  lenegcon1  8196  lenegcon2  8197  addge01  8202  addge02  8203  suble0  8206  leaddle0  8207  lesub0  8209  eqord2  8214  sublt0d  8300  recexre  8308  reaplt  8318  reapltxor  8319  reapneg  8327  remulext1  8329  apreim  8333  apcotr  8337  apadd2  8339  addext  8340  apsub1  8372  mulcanap2d  8391  diveqap0  8410  diveqap1  8433  apmul2  8517  ltmul2  8582  lemul2  8583  ltmulgt11  8590  ltmulgt12  8591  gt0div  8596  ge0div  8597  ltmuldiv  8600  ltrec1  8614  lerec2  8615  ledivdiv  8616  ltdiv23  8618  lediv23  8619  suprleubex  8680  creur  8685  creui  8686  nn1suc  8707  nnrecl  8943  znnsub  9073  zgt0ge1  9080  zltlen  9097  nn0n0n1ge2b  9098  nn0le2is012  9101  btwnnz  9113  gtndiv  9114  prime  9118  eluz2  9300  indstr2  9371  negm  9375  nn01to3  9377  qapne  9399  qltlen  9400  qreccl  9402  divlt1lt  9479  divle1le  9480  nnledivrp  9521  xnn0xadd0  9618  xltadd2  9628  xsubge0  9632  xlesubadd  9634  iccid  9676  elioc2  9687  elico2  9688  elicc2  9689  elfz2  9765  fzen  9791  fzsubel  9808  elfzp1  9820  fzpr  9825  fzrevral2  9854  fzrevral3  9855  nn0disj  9883  2ffzeq  9886  fzosplitsni  9980  fvinim0ffz  9986  ioo0  10005  ico0  10007  ioc0  10008  modq0  10070  negqmod0  10072  zmodidfzo  10094  frecuzrdgtcl  10153  nn0ennn  10174  sq11  10333  nn0le2msqd  10433  nn0opth2d  10437  hashen  10498  zfz1isolem1  10551  zfz1iso  10552  2shfti  10571  cjap  10646  cnreim  10718  rexfiuz  10729  rexanuz2  10731  abs00ap  10802  absext  10803  sqabs  10822  abslt  10828  absle  10829  absdiflt  10832  absdifle  10833  lenegsq  10835  minmax  10969  ltmininf  10974  xrminmax  11002  xrmin1inf  11004  xrmin2inf  11005  xrltmininf  11007  xrlemininf  11008  clim  11018  clim0c  11023  climrecvg1n  11085  zsumdc  11121  fsum2dlemstep  11171  binomlem  11220  pwm1geoserap1  11245  efieq  11369  sin01bnd  11391  cos01bnd  11392  dvdsval2  11423  zdvdsdc  11441  modmulconst  11452  dvdsaddr  11464  dvdsabseq  11472  fzocongeq  11483  zeo3  11492  odd2np1  11497  oddp1d2  11514  zob  11515  oddm1d2  11516  nnoddm1d2  11534  divalgb  11549  divalgmod  11551  modremain  11553  gcdn0gt0  11593  bezoutlemstep  11612  dvdssq  11646  nn0seqcvgd  11649  algcvgblem  11657  lcmdvds  11687  lcmgcdeq  11691  coprmdvds  11700  qredeq  11704  congr  11708  isprm2  11725  isprm3  11726  prmdvdsexp  11753  prmdvdsexpb  11754  prmexpb  11756  prmfac1  11757  cncongrprm  11762  oddpwdclemxy  11774  oddpwdclemodd  11777  qnumdenbi  11797  qnumgt0  11803  hashdvds  11824  crth  11827  oddennn  11832  ctinfomlemom  11867  istopg  12093  eltg  12148  eltg2  12149  tgss2  12175  bastop1  12179  bastop2  12180  iscld  12199  isnei  12240  neiint  12241  iscn  12293  iscnp  12295  iscnp3  12299  tgcn  12304  ssidcn  12306  lmbr2  12310  lmbrf  12311  cnnei  12328  cnrest2  12332  eltx  12355  imasnopn  12395  ispsmet  12419  ismet  12440  isxmet  12441  metn0  12474  xmetres2  12475  elbl3ps  12490  elbl3  12491  xblpnfps  12494  xblpnf  12495  elmopn2  12545  metss  12590  bdxmet  12597  metrest  12602  xmetxp  12603  xmetxpbl  12604  metcnp3  12607  metcnp  12608  metcnp2  12609  metcn  12610  txmetcnp  12614  txmetcn  12615  metcnpd  12616  bl2ioo  12638  addcncntoplem  12647  elcncf  12656  elcncf2  12657  ivthdec  12718  ellimc3apf  12725  cnlimcim  12736  dveflem  12782  sincosq2sgn  12835  sinq12gt0  12838  cbvrald  12922  bj-nalset  13020  bj-sels  13039  bj-nnelirr  13078  isomninnlem  13152
  Copyright terms: Public domain W3C validator