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

Theorem sylbid 143
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
sylbid.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
sylbid  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 136 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 44 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
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr4d  196  nlimsucg  4318  poltletr  4753  xp11m  4787  fvmptdf  5286  eusvobj2  5526  ovmpt2df  5660  f1o2ndf1  5877  smoiso  5948  nnsseleq  6110  ecopovtrn  6234  ecopovtrng  6237  dom2lem  6283  fundmen  6317  fidifsnen  6362  findcard2  6377  findcard2s  6378  supisoex  6413  ordiso2  6415  addcanpig  6490  mulcanpig  6491  addnidpig  6492  ordpipqqs  6530  ltexnqq  6564  prarloclemlo  6650  genpcdl  6675  genpcuu  6676  mulnqprl  6724  mulnqpru  6725  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  distrlem5prl  6742  distrlem5pru  6743  ltsopr  6752  ltexprlemfl  6765  ltexprlemfu  6767  recexprlemss1l  6791  recexprlemss1u  6792  aptiprleml  6795  ltsrprg  6890  lttrsr  6905  mulextsr1lem  6922  axapti  7149  cnegexlem1  7249  le2add  7513  lt2add  7514  ltleadd  7515  lt2sub  7529  le2sub  7530  recexre  7643  reapti  7644  apreap  7652  reapcotr  7663  remulext1  7664  apreim  7668  apcotr  7672  mulext2  7678  recexap  7708  addltmul  8218  elnnz  8312  zleloe  8349  nn0n0n1ge2b  8378  nn0lt2  8380  zextlt  8390  uzind2  8409  eluzdc  8644  qreccl  8674  xltnegi  8849  iccid  8895  icoshft  8959  zltaddlt1le  8975  fzofzim  9146  qbtwnxr  9214  flqeqceilz  9268  modqmuladdnn0  9318  modfzo0difsn  9345  addmodlteq  9348  frec2uzrand  9355  frecuzrdgfn  9362  facdiv  9606  facwordi  9608  faclbnd  9609  bcpasc  9634  recvguniq  9822  abs00ap  9889  absext  9890  absnid  9900  cau3lem  9941  climuni  10045  2clim  10053  dvdsmultr2  10147  dvdsleabs  10157  odd2np1lem  10183  odd2np1  10184  ltoddhalfle  10205  halfleoddlt  10206  m1expo  10212  nn0enne  10214  nn0ehalf  10215  nn0o1gt2  10217  flodddiv4  10246  algcvgblem  10271  ialgcvga  10273
  Copyright terms: Public domain W3C validator