Theorem sylibrd 249

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	|- ( ph -> ( ps -> ch ) )
sylibrd.2	|- ( ph -> ( th <-> ch ) )

Assertion

Ref	Expression
sylibrd	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibrd.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	2	biimprd 238	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 47	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3imtr4d  283  sbciegft  3466  eqsbc3rOLD  3493  opeldmd  5327  elreldm  5350  ordtr2  5768  ssimaex  6263  fliftfun  6562  isopolem  6595  isosolem  6597  ordsucss  7018  f1oweALT  7152  fnse  7294  brtpos  7361  issmo2  7446  seqomlem1  7545  omcl  7616  oecl  7617  oawordeulem  7634  oaass  7641  omordi  7646  omord  7648  odi  7659  oen0  7666  oeordi  7667  oeordsuc  7674  nnmcl  7692  nnecl  7693  nnmordi  7711  nnmord  7712  nnmwordri  7716  nnaordex  7718  swoord1  7773  ecopovtrn  7850  f1domg  7975  pw2f1olem  8064  domtriord  8106  mapen  8124  mapxpen  8126  mapunen  8129  nndomo  8154  inficl  8331  supmo  8358  infmo  8401  inf3lem6  8530  cantnflem1  8586  tcmin  8617  tcrank  8747  cardne  8791  cardlim  8798  cardsdomel  8800  carduni  8807  alephord  8898  cardinfima  8920  dfac5lem4  8949  infdif2  9032  cofsmo  9091  cfcoflem  9094  infpssrlem4  9128  infpssrlem5  9129  fin4en1  9131  isfin2-2  9141  enfin2i  9143  fin23lem27  9150  isf32lem12  9186  isf34lem6  9202  domtriomlem  9264  cardmin  9386  fpwwe2lem12  9463  inar1  9597  gruiun  9621  ltsonq  9791  prub  9816  reclem3pr  9871  mulcmpblnr  9892  mulgt0sr  9926  axpre-sup  9990  leltadd  10512  infm3  10982  peano5nni  11023  zextle  11450  prime  11458  uzin  11720  ublbneg  11773  zbtwnre  11786  mul2lt0bi  11936  xrre2  12001  xralrple  12036  xmulneg1  12099  supxrbnd  12158  supxrgtmnf  12159  fzrevral  12425  flge  12606  ceile  12648  modadd1  12707  modmul1  12723  modsumfzodifsn  12743  seqcl2  12819  facdiv  13074  hashss  13197  hash2exprb  13253  elfzelfzccat  13364  repswswrd  13531  cshf1  13556  cshwcsh2id  13574  rlim2lt  14228  rlim3  14229  o1lo1  14268  climshftlem  14305  o1co  14317  o1of2  14343  isercolllem2  14396  isercoll  14398  caucvgrlem2  14405  climcndslem2  14582  sqrt2irr  14979  dvds2lem  14994  dvdsle  15032  dvdsfac  15048  ltoddhalfle  15085  divalglem0  15116  ndvdsadd  15134  bitsinv1lem  15163  sadcaddlem  15179  dvdslegcd  15226  bezoutlem2  15257  bezoutlem4  15259  gcdzeq  15271  algcvga  15292  rpdvds  15374  cncongr1  15381  cncongr2  15382  prmind2  15398  isprm6  15426  rpexp  15432  eulerthlem2  15487  pclem  15543  pceulem  15550  pc2dvds  15583  fldivp1  15601  infpnlem1  15614  prmunb  15618  mrieqv2d  16299  plttr  16970  clatl  17116  issubg4  17613  gexdvds  17999  pgpssslw  18029  sylow2alem2  18033  efgs1b  18149  efgsfo  18152  lspindpi  19132  pf1ind  19719  psgnodpm  19934  psgndif  19948  obselocv  20072  mdetunilem9  20426  fiinbas  20756  bastg  20770  tgcl  20773  opnssneib  20919  clslp  20952  tgcnp  21057  iscnp4  21067  cncls2  21077  cncls  21078  cnntr  21079  cnpresti  21092  lmss  21102  lmcnp  21108  cmpsub  21203  tgcmp  21204  dfconn2  21222  t1connperf  21239  1stcfb  21248  1stcrest  21256  kgenss  21346  llycmpkgen2  21353  txdis  21435  qtoptop2  21502  kqt0lem  21539  isr0  21540  regr1lem2  21543  cmphaushmeo  21603  fbun  21644  ssfg  21676  fgtr  21694  ufildr  21735  cnpflf  21805  fclsnei  21823  flimfnfcls  21832  fclscmp  21834  ufilcmp  21836  cnpfcf  21845  alexsublem  21848  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem3  21858  tgphaus  21920  tgpt1  21921  tsmsres  21947  imasdsf1olem  22178  xblss2ps  22206  xblss2  22207  blsscls2  22309  metequiv2  22315  stdbdxmet  22320  nmoi  22532  reconn  22631  mulc1cncf  22708  cncfco  22710  iccpnfhmeo  22744  xrhmeo  22745  evth  22758  pi1grplem  22849  fgcfil  23069  ivthlem2  23221  ivthlem3  23222  ovolicc2lem4  23288  voliunlem1  23318  ioombl1lem4  23329  itg2gt0  23527  limcco  23657  lhop1  23777  tdeglem4  23820  plypf1  23968  coeeulem  23980  coeidlem  23993  coeid3  23996  plymul0or  24036  dvnply2  24042  plydivex  24052  vieta1lem2  24066  plyexmo  24068  aaliou3lem2  24098  ulmss  24151  ulmdvlem3  24156  iblulm  24161  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  logcnlem5  24392  dcubic  24573  amgm  24717  isnsqf  24861  mumullem2  24906  chtublem  24936  chtub  24937  fsumvma2  24939  vmasum  24941  dchrfi  24980  bposlem1  25009  bposlem3  25011  bposlem7  25015  lgsdir  25057  lgsquadlem2  25106  2sqlem8a  25150  2sqlem10  25153  dchrisum0flb  25199  pntpbnd1  25275  pntlemf  25294  pntlem3  25298  axeuclid  25843  uspgrushgr  26070  uspgrupgr  26071  usgruspgr  26073  usgr2pth  26660  crctcshwlkn0lem5  26706  wwlksnext  26788  wwlksnextsur  26795  clwwisshclwwslemlem  26926  lnon0  27653  normpyc  28003  ocsh  28142  ocorth  28150  ococss  28152  shsel2  28181  hsupss  28200  pjhth  28252  shlub  28273  cm2j  28479  lnfncnbd  28916  riesz1  28924  rnbra  28966  leopadd  28991  leopmuli  28992  hstles  29090  stge1i  29097  stle0i  29098  dmdbr5  29167  ssmd2  29171  superpos  29213  chcv1  29214  atoml2i  29242  chirredlem2  29250  atcvat3i  29255  mdsymlem5  29266  mdsymlem6  29267  sumdmdii  29274  sumdmdlem2  29278  isarchiofld  29817  sqsscirc2  29955  cnre2csqlem  29956  xrge0iifiso  29981  sigaclci  30195  omssubadd  30362  eulerpartlemb  30430  ballotlemimin  30567  ballotlem7  30597  cvmlift2lem12  31296  dfon2lem8  31695  soseq  31751  segconeq  32117  ifscgr  32151  brofs2  32184  brifs2  32185  endofsegid  32192  dissneqlem  33187  tan2h  33401  matunitlindflem2  33406  poimirlem31  33440  poimir  33442  fzmul  33537  fdc  33541  incsequz2  33545  sstotbnd2  33573  sstotbnd3  33575  totbndbnd  33588  isexid2  33654  ispridl2  33837  mpt2bi123f  33971  riotasvd  34242  lsator0sp  34288  lssatle  34302  lshpset2N  34406  lkrlspeqN  34458  omllaw2N  34531  cmtbr3N  34541  lecmtN  34543  cvlcvr1  34626  cvrval4N  34700  cvrat3  34728  3noncolr2  34735  4noncolr3  34739  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4  34750  3dimlem4OLDN  34751  llncvrlpln  34844  lplncvrlvol  34902  snatpsubN  35036  linepsubN  35038  pmapjat1  35139  pclfinclN  35236  pl42N  35269  ltrneq2  35434  cdleme7aa  35529  cdleme18d  35582  cdleme21b  35614  trlord  35857  trlcoat  36011  dochkrshp  36675  lcfl8  36791  irrapxlem2  37387  pell14qrdich  37433  monotoddzz  37508  pw2f1ocnv  37604  iocinico  37797  sbcim2g  38748  stoweidlem62  40279  elfzelfzlble  41331