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

Theorem sylbid 150
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 144 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  3imtr4d  203  ifnebibdc  3601  nlimsucg  4599  poltletr  5067  xp11m  5105  fvmptdf  5646  elfvmptrab1  5653  eusvobj2  5905  ovmpodf  6051  elovmporab  6120  elovmporab1w  6121  f1o2ndf1  6283  smoiso  6357  nnsseleq  6556  ecopovtrn  6688  ecopovtrng  6691  dom2lem  6828  fundmen  6862  fidifsnen  6928  findcard2  6947  findcard2s  6948  supisoex  7070  infglbti  7086  ordiso2  7096  updjud  7143  difinfsnlem  7160  enomnilem  7199  enmkvlem  7222  netap  7316  2omotaplemap  7319  cc2lem  7328  addcanpig  7396  mulcanpig  7397  addnidpig  7398  ordpipqqs  7436  ltexnqq  7470  prarloclemlo  7556  genpcdl  7581  genpcuu  7582  mulnqprl  7630  mulnqpru  7631  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  distrlem5prl  7648  distrlem5pru  7649  ltsopr  7658  ltexprlemfl  7671  ltexprlemfu  7673  recexprlemss1l  7697  recexprlemss1u  7698  aptiprleml  7701  ltsrprg  7809  lttrsr  7824  mulextsr1lem  7842  axapti  8092  cnegexlem1  8196  le2add  8465  lt2add  8466  ltleadd  8467  lt2sub  8481  le2sub  8482  recexre  8599  reapti  8600  apreap  8608  reapcotr  8619  remulext1  8620  apreim  8624  apcotr  8628  mulext2  8634  recexap  8674  addltmul  9222  elnnz  9330  zleloe  9367  difgtsumgt  9389  nn0n0n1ge2b  9399  nn0lt2  9401  nn0le2is012  9402  zextlt  9412  uzind2  9432  supinfneg  9663  infsupneg  9664  eluzdc  9678  qreccl  9710  elpq  9717  xltnegi  9904  xnn0lenn0nn0  9934  iccid  9994  icoshft  10059  zltaddlt1le  10076  fzofzim  10258  qbtwnxr  10329  flqeqceilz  10392  modqmuladdnn0  10442  modfzo0difsn  10469  addmodlteq  10472  frec2uzrand  10479  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seqf1oglem1  10593  facdiv  10812  facwordi  10814  faclbnd  10815  bcpasc  10840  seq3coll  10916  fstwrdne  10955  elovmpowrd  10958  recvguniq  11142  abs00ap  11209  absext  11210  absnid  11220  cau3lem  11261  climuni  11439  2clim  11447  summodc  11529  fisumss  11538  fsumabs  11611  mertenslem2  11682  fprodssdc  11736  reeff1  11846  efieq1re  11918  dvdsmultr2  11979  dvdsleabs  11990  odd2np1lem  12016  odd2np1  12017  ltoddhalfle  12037  halfleoddlt  12038  m1expo  12044  nn0enne  12046  nn0ehalf  12047  nn0o1gt2  12049  flodddiv4  12078  zeqzmulgcd  12110  gcdneg  12122  gcdaddm  12124  bezoutlemaz  12143  bezoutlembz  12144  dfgcd2  12154  gcddiv  12159  dvdssqim  12164  algcvgblem  12190  algcvga  12192  lcmneg  12215  coprmgcdb  12229  coprmdvds2  12234  qredeq  12237  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  prmind2  12261  dvdsnprmd  12266  prmgt1  12273  nprmdvds1  12281  divgcdodd  12284  euclemma  12287  prmdvdsexpr  12291  prmfac1  12293  prmndvdsfaclt  12297  crth  12365  eulerthlemh  12372  fermltl  12375  nnnn0modprm0  12396  coprimeprodsq2  12399  pythagtriplem2  12407  pcpremul  12434  pcdvdsb  12461  pc2dvds  12471  pc11  12472  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  difsqpwdvds  12479  pcfac  12491  oddprmdvds  12495  prmpwdvds  12496  1arith  12508  4sqlem11  12542  4sqlem12  12543  imasaddfnlemg  12900  erlecpbl  12918  xpsff1o  12935  grp1inv  13182  imasgrp2  13183  ghmpreima  13339  imasabl  13409  imasrng  13455  imasring  13563  dvdsrtr  13600  dvdsrmul1  13601  unitgrp  13615  znidomb  14157  tgtop  14247  tgidm  14253  neipsm  14333  restbasg  14347  tgrest  14348  tgcn  14387  tgcnp  14388  cnconst2  14412  cnconst  14413  cnptopresti  14417  txbasval  14446  txcnp  14450  txdis1cn  14457  bldisj  14580  xblm  14596  blssps  14606  blss  14607  blin2  14611  cnlimcim  14850  dveflem  14905  sincosq3sgn  15004  sincosq4sgn  15005  coseq0q4123  15010  ioocosf1o  15030  logbgcd1irr  15140  zabsle1  15156  lgsdir2lem5  15189  lgsne0  15195  lgsdirnn0  15204  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem2  15228  lgsquadlem1  15234  2lgslem1a1  15243  2lgslem1b  15246  2lgslem1c  15247  2lgs  15261  2lgsoddprmlem2  15263  uzdcinzz  15360  subctctexmid  15561
  Copyright terms: Public domain W3C validator