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

Theorem sylbid 148
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 142 . 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 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr4d  201  nlimsucg  4372  poltletr  4819  xp11m  4856  fvmptdf  5374  eusvobj2  5620  ovmpt2df  5758  f1o2ndf1  5975  smoiso  6049  nnsseleq  6244  ecopovtrn  6369  ecopovtrng  6372  dom2lem  6469  fundmen  6503  fidifsnen  6566  findcard2  6585  findcard2s  6586  supisoex  6683  infglbti  6699  ordiso2  6707  updjud  6752  enomnilem  6773  addcanpig  6872  mulcanpig  6873  addnidpig  6874  ordpipqqs  6912  ltexnqq  6946  prarloclemlo  7032  genpcdl  7057  genpcuu  7058  mulnqprl  7106  mulnqpru  7107  distrlem1prl  7120  distrlem1pru  7121  distrlem4prl  7122  distrlem4pru  7123  distrlem5prl  7124  distrlem5pru  7125  ltsopr  7134  ltexprlemfl  7147  ltexprlemfu  7149  recexprlemss1l  7173  recexprlemss1u  7174  aptiprleml  7177  ltsrprg  7272  lttrsr  7287  mulextsr1lem  7304  axapti  7536  cnegexlem1  7636  le2add  7901  lt2add  7902  ltleadd  7903  lt2sub  7917  le2sub  7918  recexre  8031  reapti  8032  apreap  8040  reapcotr  8051  remulext1  8052  apreim  8056  apcotr  8060  mulext2  8066  recexap  8096  addltmul  8622  elnnz  8730  zleloe  8767  nn0n0n1ge2b  8796  nn0lt2  8798  zextlt  8808  uzind2  8828  supinfneg  9052  infsupneg  9053  eluzdc  9066  qreccl  9096  xltnegi  9266  iccid  9312  icoshft  9376  zltaddlt1le  9392  fzofzim  9564  qbtwnxr  9634  flqeqceilz  9690  modqmuladdnn0  9740  modfzo0difsn  9767  addmodlteq  9770  frec2uzrand  9777  frecuzrdgtcl  9784  frecuzrdgfunlem  9791  facdiv  10111  facwordi  10113  faclbnd  10114  bcpasc  10139  iseqcoll  10212  recvguniq  10393  abs00ap  10460  absext  10461  absnid  10471  cau3lem  10512  climuni  10645  2clim  10653  isummo  10737  fisumss  10748  fsumabs  10822  dvdsmultr2  10918  dvdsleabs  10928  odd2np1lem  10954  odd2np1  10955  ltoddhalfle  10975  halfleoddlt  10976  m1expo  10982  nn0enne  10984  nn0ehalf  10985  nn0o1gt2  10987  flodddiv4  11016  zeqzmulgcd  11044  gcdneg  11055  gcdaddm  11057  bezoutlemaz  11074  bezoutlembz  11075  dfgcd2  11085  gcddiv  11090  dvdssqim  11095  algcvgblem  11113  ialgcvga  11115  lcmneg  11138  coprmgcdb  11152  coprmdvds2  11157  qredeq  11160  divgcdcoprm0  11165  divgcdcoprmex  11166  cncongr1  11167  cncongr2  11168  prmind2  11184  dvdsnprmd  11189  prmgt1  11195  nprmdvds1  11203  divgcdodd  11204  euclemma  11207  prmdvdsexpr  11211  prmfac1  11213  prmndvdsfaclt  11217  crth  11282  uzdcinzz  11344
  Copyright terms: Public domain W3C validator