Theorem sylibrd 259

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

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr4d  294  sbciegftOLD  3780  opeldmd  5863  elreldm  5892  predtrss  6288  ordtr2  6370  ssimaex  6927  fliftfun  7268  isopolem  7301  isosolem  7303  ordsucss  7770  f1oweALT  7926  fnse  8085  soseq  8111  brtpos  8187  issmo2  8291  seqomlem1  8391  omcl  8473  oecl  8474  oawordeulem  8491  oaass  8498  omordi  8503  omord  8505  odi  8516  oen0  8524  oeordi  8525  oeordsuc  8532  nnmcl  8550  nnecl  8551  nnmordi  8569  nnmord  8570  nnmwordri  8574  nnaordex  8576  swoord1  8678  ecopovtrn  8769  f1domg  8920  pw2f1olem  9021  domtriord  9063  mapen  9081  mapxpen  9083  mapunen  9086  nndomog  9149  onomeneq  9150  inficl  9340  supmo  9367  infmo  9412  inf3lem6  9554  cantnflem1  9610  tcmin  9660  tcrank  9808  cardne  9889  cardlim  9896  cardsdomel  9898  carduni  9905  alephord  9997  cardinfima  10019  dfac5lem4  10048  dfac5lem4OLD  10050  infdif2  10131  cofsmo  10191  cfcoflem  10194  infpssrlem4  10228  infpssrlem5  10229  fin4en1  10231  isfin2-2  10241  enfin2i  10243  fin23lem27  10250  isf32lem12  10286  isf34lem6  10302  domtriomlem  10364  cardmin  10486  fpwwe2lem11  10564  inar1  10698  gruiun  10722  ltsonq  10892  prub  10917  reclem3pr  10972  mulcmpblnr  10994  mulgt0sr  11028  axpre-sup  11092  leltadd  11633  infm3  12113  peano5nni  12160  zextle  12577  prime  12585  uzin  12799  ublbneg  12858  zbtwnre  12871  mul2lt0bi  13025  xrre2  13097  xralrple  13132  xmulneg1  13196  supxrbnd  13255  supxrgtmnf  13256  fzrevral  13540  flge  13737  ceile  13781  modadd1  13840  modmul1  13859  modsumfzodifsn  13879  seqcl2  13955  facdiv  14222  hashss  14344  hash2exprb  14406  elfzelfzccat  14515  repswswrd  14719  cshf1  14745  cshwcsh2id  14763  rlim2lt  15432  rlim3  15433  o1lo1  15472  climshftlem  15509  o1co  15521  o1of2  15548  isercolllem2  15601  isercoll  15603  caucvgrlem2  15610  climcndslem2  15785  sqrt2irr  16186  dvds2lem  16207  dvdsle  16249  dvdsfac  16265  ltoddhalfle  16300  divalglem0  16332  ndvdsadd  16349  bitsinv1lem  16380  sadcaddlem  16396  dvdslegcd  16443  bezoutlem2  16479  bezoutlem4  16481  gcdzeq  16491  algcvga  16518  rpdvds  16599  cncongr1  16606  cncongr2  16607  prmind2  16624  isprm6  16653  rpexp  16661  eulerthlem2  16721  pclem  16778  pceulem  16785  pc2dvds  16819  fldivp1  16837  infpnlem1  16850  prmunb  16854  mrieqv2d  17574  plttr  18275  clatl  18443  issubg4  19087  gexdvds  19525  pgpssslw  19555  sylow2alem2  19559  efgs1b  19677  efgsfo  19680  imasabl  19817  lspindpi  21099  psgnodpm  21555  psgndif  21569  obselocv  21695  pf1ind  22311  mdetunilem9  22576  fiinbas  22908  bastg  22922  tgcl  22925  opnssneib  23071  clslp  23104  tgcnp  23209  iscnp4  23219  cncls2  23229  cncls  23230  cnntr  23231  cnpresti  23244  lmss  23254  lmcnp  23260  cmpsub  23356  tgcmp  23357  dfconn2  23375  t1connperf  23392  1stcfb  23401  1stcrest  23409  kgenss  23499  llycmpkgen2  23506  txdis  23588  qtoptop2  23655  kqt0lem  23692  isr0  23693  regr1lem2  23696  cmphaushmeo  23756  fbun  23796  ssfg  23828  fgtr  23846  ufildr  23887  cnpflf  23957  fclsnei  23975  flimfnfcls  23984  fclscmp  23986  ufilcmp  23988  cnpfcf  23997  alexsublem  24000  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem3  24010  tgphaus  24073  tgpt1  24074  tsmsres  24100  imasdsf1olem  24329  xblss2ps  24357  xblss2  24358  blsscls2  24460  metequiv2  24466  stdbdxmet  24471  nmoi  24684  reconn  24785  mulc1cncf  24866  cncfco  24868  iccpnfhmeo  24911  xrhmeo  24912  evth  24926  pi1grplem  25017  fgcfil  25239  ivthlem2  25421  ivthlem3  25422  ovolicc2lem4  25489  voliunlem1  25519  ioombl1lem4  25530  itg2gt0  25729  limcco  25862  lhop1  25987  tdeglem4  26033  plypf1  26185  coeeulem  26197  coeidlem  26210  coeid3  26213  plymul0or  26256  dvnply2  26263  plydivex  26273  vieta1lem2  26287  plyexmo  26289  aaliou3lem2  26319  ulmss  26374  ulmdvlem3  26379  iblulm  26384  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  logcnlem5  26623  dcubic  26824  amgm  26969  isnsqf  27113  mumullem2  27158  chtublem  27190  chtub  27191  fsumvma2  27193  vmasum  27195  dchrfi  27234  bposlem1  27263  bposlem3  27265  bposlem7  27269  lgsdir  27311  lgsquadlem2  27360  2sqlem8a  27404  2sqlem10  27407  dchrisum0flb  27489  pntpbnd1  27565  pntlemf  27584  pntlem3  27588  addonbday  28287  peano5uzs  28412  axeuclid  29048  uspgrushgr  29262  uspgrupgr  29263  usgruspgr  29265  usgr2pth  29849  crctcshwlkn0lem5  29899  wwlksnext  29978  wwlksnextsurj  29985  clwwlkccatlem  30076  clwlkclwwlkf  30095  clwwisshclwwslemlem  30100  lnon0  30885  normpyc  31233  ocsh  31370  ocorth  31378  ococss  31380  shsel2  31409  hsupss  31428  pjhth  31480  shlub  31501  cm2j  31707  lnfncnbd  32144  riesz1  32152  rnbra  32194  leopadd  32219  leopmuli  32220  hstles  32318  stge1i  32325  stle0i  32326  dmdbr5  32395  ssmd2  32399  superpos  32441  chcv1  32442  atoml2i  32470  chirredlem2  32478  atcvat3i  32483  mdsymlem5  32494  mdsymlem6  32495  sumdmdii  32502  sumdmdlem2  32506  isarchiofld  33292  sqsscirc2  34086  cnre2csqlem  34087  xrge0iifiso  34112  sigaclci  34309  omssubadd  34477  eulerpartlemb  34545  ballotlemimin  34683  ballotlem7  34713  fineqvac  35291  fineqvinfep  35300  vonf1owev  35321  subgrwlk  35345  cusgracyclt3v  35369  cvmlift2lem12  35527  fmlasucdisj  35612  dfon2lem8  36001  segconeq  36223  ifscgr  36257  brofs2  36290  brifs2  36291  endofsegid  36298  dissneqlem  37584  rdgellim  37620  fvineqsneq  37656  tan2h  37852  matunitlindflem2  37857  poimirlem31  37891  poimir  37893  fzmul  37981  fdc  37985  incsequz2  37989  sstotbnd2  38014  sstotbnd3  38016  totbndbnd  38029  isexid2  38095  ispridl2  38278  mpobi123f  38402  disjlem18  39143  disjdmqsss  39145  eldisjs6  39180  riotasvd  39321  lsator0sp  39366  lssatle  39380  lshpset2N  39484  lkrlspeqN  39536  omllaw2N  39609  cmtbr3N  39619  lecmtN  39621  cvlcvr1  39704  cvrval4N  39779  cvrat3  39807  3noncolr2  39814  4noncolr3  39818  3dimlem3  39826  3dimlem3OLDN  39827  3dimlem4  39829  3dimlem4OLDN  39830  llncvrlpln  39923  lplncvrlvol  39981  snatpsubN  40115  linepsubN  40117  pmapjat1  40218  pclfinclN  40315  pl42N  40348  ltrneq2  40513  cdleme7aa  40607  cdleme18d  40660  cdleme21b  40691  trlord  40934  trlcoat  41088  dochkrshp  41751  lcfl8  41867  mulgt0con1dlem  42828  irrapxlem2  43169  pell14qrdich  43215  monotoddzz  43289  pw2f1ocnv  43383  iocinico  43558  ordnexbtwnsuc  43613  tfsconcat0i  43691  naddwordnexlem4  43747  harval3  43883  sbcim2g  44883  stoweidlem62  46409  elfzelfzlble  47670  pgnbgreunbgrlem1  48462  pgnbgreunbgrlem4  48468  1arymaptf1  48991  2arymaptf1  49002  eenglngeehlnmlem2  49087  mpbiran3d  49145  opnneil  49258