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

Theorem bitrd 177
Description: Deduction form of bitri 173. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
Hypotheses
Ref Expression
bitrd.1
bitrd.2
Assertion
Ref Expression
bitrd

Proof of Theorem bitrd
StepHypRef Expression
1 bitrd.1 . . . 4
21pm5.74i 169 . . 3
3 bitrd.2 . . . 4
43pm5.74i 169 . . 3
52, 4bitri 173 . 2
65pm5.74ri 170 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bitr2d  178  bitr3d  179  bitr4d  180  syl5bb  181  syl6bb  185  3bitrd  203  3bitr2d  205  3bitr3d  207  3bitr4d  209  imbi12d  223  bibi12d  224  sylan9bb  435  anbi12d  442  orbi12d  706  con1biidc  770  pm4.54dc  804  dn1dc  866  dedlem0a  874  xorbi12d  1271  nbbndc  1282  eleq12d  2105  neeq12d  2220  neleq12d  2297  raleqbi1dv  2507  rexeqbi1dv  2508  reueqd  2509  rmoeqd  2510  raleqbidv  2511  rexeqbidv  2512  raleqbidva  2513  rexeqbidva  2514  eueq3dc  2709  sbc19.21g  2820  sbcabel  2833  sbcel1g  2863  sbceq1g  2864  sbcel2g  2865  sbceq2g  2866  sbccsb2g  2873  sbcco3g  2897  sseq12d  2968  psseq12d  3032  raaanlem  3320  sbcssg  3324  ralsng  3402  rexsng  3403  2ralunsn  3560  csbunig  3579  disjeq12d  3745  breq123d  3769  sbcbr12g  3805  sbcbr1g  3806  sbcbr2g  3807  treq  3851  nalset  3878  copsex4g  3975  sucelon  4195  posng  4355  csbxpg  4364  sbcrel  4369  csbcnvg  4462  eliniseg  4638  brcodir  4655  csbrng  4725  sbcfung  4868  fneq12d  4934  feq12d  4979  feq123d  4980  sbcfng  4987  sbcfg  4988  f1osng  5110  csbfv12g  5152  funimass4  5167  dmfco  5184  eqfnfv  5208  eqfnfv2  5209  fneqeql2  5219  fvimacnvi  5224  funimass3  5226  fniniseg  5230  rexsupp  5234  unpreima  5235  ralrnmpt  5252  rexrnmpt  5253  dffo3  5257  fmptco  5273  fressnfv  5293  eufnfv  5332  fnunirn  5349  dff13  5350  f1elima  5355  cocan1  5370  cocan2  5371  fliftel  5376  fliftf  5382  isoresbr  5392  isoini  5400  f1oiso  5408  f1ofveu  5443  mpt2eq123dva  5508  ovid  5559  ov  5562  ovg  5581  ovelrn  5591  caovord2d  5612  ofrfval2  5669  offveqb  5672  eqop  5745  reldm  5754  mpt2xopoveq  5796  mpt2xopovel  5797  isprmpt2  5799  tpostpos  5820  smoiso  5858  frecsuclem3  5929  nnaordr  6019  nnaword  6020  nnaordex  6036  ereq1  6049  brdifun  6069  erth2  6087  qliftfun  6124  brecop  6132  dom2lem  6188  xpcomco  6236  ltapig  6322  ltmpig  6323  nlt1pig  6325  mulcmpblnq  6352  ltsonq  6382  lt2addnq  6388  archnqq  6400  prarloclemarch  6401  ltrnqg  6403  mulcmpblnq0  6426  preqlu  6454  genpdflem  6489  addnqprllem  6509  addnqprulem  6510  addlocprlemgt  6516  appdivnq  6543  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  distrlem4prl  6559  distrlem4pru  6560  1idprl  6565  1idpru  6566  ltexprlemloc  6580  cauappcvgprlemladdrl  6628  cauappcvgprlemladd  6629  cauappcvgprlem1  6630  addcmpblnr  6647  lttrsr  6670  ltsosr  6672  ltasrg  6678  mulextsr1  6687  ltresr  6716  cnegexlem1  6963  negeu  6979  subadd2  6992  subcan2  7012  ltadd1  7199  leadd2  7201  ltsubadd  7202  lesubadd  7204  ltaddsub2  7207  leaddsub2  7209  ltaddpos  7222  lesub2  7227  ltsub2  7229  ltnegcon1  7233  ltnegcon2  7234  lenegcon1  7236  lenegcon2  7237  addge01  7242  addge02  7243  suble0  7246  leaddle0  7247  lesub0  7249  recexre  7342  reaplt  7352  reapltxor  7353  reapneg  7361  remulext1  7363  apreim  7367  apcotr  7371  apadd2  7373  addext  7374  mulcanap2d  7405  diveqap0  7423  diveqap1  7444  ltmul2  7583  lemul2  7584  ltmulgt11  7591  ltmulgt12  7592  gt0div  7597  ge0div  7598  ltmuldiv  7601  ltrec1  7615  lerec2  7616  ledivdiv  7617  ltdiv23  7619  lediv23  7620  creur  7672  creui  7673  nn1suc  7694  nnrecl  7935  znnsub  8052  zgt0ge1  8058  zltlen  8075  nn0n0n1ge2b  8076  btwnnz  8090  gtndiv  8091  prime  8093  eluz2  8235  indstr2  8302  negm  8306  nn01to3  8308  qapne  8330  qreccl  8331  iccid  8544  elioc2  8555  elico2  8556  elicc2  8557  elfz2  8631  fzen  8657  fzsubel  8673  elfzp1  8684  fzpr  8689  fzrevral2  8718  fzrevral3  8719  nn0disj  8745  2ffzeq  8748  fzosplitsni  8841  frecuzrdgfn  8859  nn0ennn  8870  sq11  8959  cjap  9114  cbvrald  9242  bj-nalset  9326  bj-sels  9345  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator