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 247	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4d  294  sbciegft  3814  opeldmd  5904  elreldm  5932  predtrss  6320  ordtr2  6405  ssimaex  6972  fliftfun  7304  isopolem  7337  isosolem  7339  ordsucss  7801  f1oweALT  7954  fnse  8114  soseq  8140  brtpos  8215  issmo2  8344  seqomlem1  8445  omcl  8531  oecl  8532  oawordeulem  8550  oaass  8557  omordi  8562  omord  8564  odi  8575  oen0  8582  oeordi  8583  oeordsuc  8590  nnmcl  8608  nnecl  8609  nnmordi  8627  nnmord  8628  nnmwordri  8632  nnaordex  8634  swoord1  8730  ecopovtrn  8810  f1domg  8964  pw2f1olem  9072  domtriord  9119  mapen  9137  mapxpen  9139  mapunen  9142  nndomog  9212  nndomogOLD  9222  onomeneq  9224  inficl  9416  supmo  9443  infmo  9486  inf3lem6  9624  cantnflem1  9680  tcmin  9732  tcrank  9875  cardne  9956  cardlim  9963  cardsdomel  9965  carduni  9972  alephord  10066  cardinfima  10088  dfac5lem4  10117  infdif2  10201  cofsmo  10260  cfcoflem  10263  infpssrlem4  10297  infpssrlem5  10298  fin4en1  10300  isfin2-2  10310  enfin2i  10312  fin23lem27  10319  isf32lem12  10355  isf34lem6  10371  domtriomlem  10433  cardmin  10555  fpwwe2lem11  10632  inar1  10766  gruiun  10790  ltsonq  10960  prub  10985  reclem3pr  11040  mulcmpblnr  11062  mulgt0sr  11096  axpre-sup  11160  leltadd  11694  infm3  12169  peano5nni  12211  zextle  12631  prime  12639  uzin  12858  ublbneg  12913  zbtwnre  12926  mul2lt0bi  13076  xrre2  13145  xralrple  13180  xmulneg1  13244  supxrbnd  13303  supxrgtmnf  13304  fzrevral  13582  flge  13766  ceile  13810  modadd1  13869  modmul1  13885  modsumfzodifsn  13905  seqcl2  13982  facdiv  14243  hashss  14365  hash2exprb  14428  elfzelfzccat  14526  repswswrd  14730  cshf1  14756  cshwcsh2id  14775  rlim2lt  15437  rlim3  15438  o1lo1  15477  climshftlem  15514  o1co  15526  o1of2  15553  isercolllem2  15608  isercoll  15610  caucvgrlem2  15617  climcndslem2  15792  sqrt2irr  16188  dvds2lem  16208  dvdsle  16249  dvdsfac  16265  ltoddhalfle  16300  divalglem0  16332  ndvdsadd  16349  bitsinv1lem  16378  sadcaddlem  16394  dvdslegcd  16441  bezoutlem2  16478  bezoutlem4  16480  gcdzeq  16490  algcvga  16512  rpdvds  16593  cncongr1  16600  cncongr2  16601  prmind2  16618  isprm6  16647  rpexp  16655  eulerthlem2  16711  pclem  16767  pceulem  16774  pc2dvds  16808  fldivp1  16826  infpnlem1  16839  prmunb  16843  mrieqv2d  17579  plttr  18291  clatl  18457  issubg4  19019  gexdvds  19445  pgpssslw  19475  sylow2alem2  19479  efgs1b  19597  efgsfo  19600  imasabl  19736  lspindpi  20733  psgnodpm  21125  psgndif  21139  obselocv  21267  pf1ind  21856  mdetunilem9  22104  fiinbas  22437  bastg  22451  tgcl  22454  opnssneib  22601  clslp  22634  tgcnp  22739  iscnp4  22749  cncls2  22759  cncls  22760  cnntr  22761  cnpresti  22774  lmss  22784  lmcnp  22790  cmpsub  22886  tgcmp  22887  dfconn2  22905  t1connperf  22922  1stcfb  22931  1stcrest  22939  kgenss  23029  llycmpkgen2  23036  txdis  23118  qtoptop2  23185  kqt0lem  23222  isr0  23223  regr1lem2  23226  cmphaushmeo  23286  fbun  23326  ssfg  23358  fgtr  23376  ufildr  23417  cnpflf  23487  fclsnei  23505  flimfnfcls  23514  fclscmp  23516  ufilcmp  23518  cnpfcf  23527  alexsublem  23530  alexsubALTlem3  23535  alexsubALTlem4  23536  ptcmplem3  23540  tgphaus  23603  tgpt1  23604  tsmsres  23630  imasdsf1olem  23861  xblss2ps  23889  xblss2  23890  blsscls2  23995  metequiv2  24001  stdbdxmet  24006  nmoi  24227  reconn  24326  mulc1cncf  24403  cncfco  24405  iccpnfhmeo  24443  xrhmeo  24444  evth  24457  pi1grplem  24547  fgcfil  24770  ivthlem2  24951  ivthlem3  24952  ovolicc2lem4  25019  voliunlem1  25049  ioombl1lem4  25060  itg2gt0  25260  limcco  25392  lhop1  25513  tdeglem4  25559  tdeglem4OLD  25560  plypf1  25708  coeeulem  25720  coeidlem  25733  coeid3  25736  plymul0or  25776  dvnply2  25782  plydivex  25792  vieta1lem2  25806  plyexmo  25808  aaliou3lem2  25838  ulmss  25891  ulmdvlem3  25896  iblulm  25901  sincosq2sgn  25991  sincosq3sgn  25992  sincosq4sgn  25993  logcnlem5  26136  dcubic  26331  amgm  26475  isnsqf  26619  mumullem2  26664  chtublem  26694  chtub  26695  fsumvma2  26697  vmasum  26699  dchrfi  26738  bposlem1  26767  bposlem3  26769  bposlem7  26773  lgsdir  26815  lgsquadlem2  26864  2sqlem8a  26908  2sqlem10  26911  dchrisum0flb  26993  pntpbnd1  27069  pntlemf  27088  pntlem3  27092  axeuclid  28201  uspgrushgr  28415  uspgrupgr  28416  usgruspgr  28418  usgr2pth  29001  crctcshwlkn0lem5  29048  wwlksnext  29127  wwlksnextsurj  29134  clwwlkccatlem  29222  clwlkclwwlkf  29241  clwwisshclwwslemlem  29246  lnon0  30029  normpyc  30377  ocsh  30514  ocorth  30522  ococss  30524  shsel2  30553  hsupss  30572  pjhth  30624  shlub  30645  cm2j  30851  lnfncnbd  31288  riesz1  31296  rnbra  31338  leopadd  31363  leopmuli  31364  hstles  31462  stge1i  31469  stle0i  31470  dmdbr5  31539  ssmd2  31543  superpos  31585  chcv1  31586  atoml2i  31614  chirredlem2  31622  atcvat3i  31627  mdsymlem5  31638  mdsymlem6  31639  sumdmdii  31646  sumdmdlem2  31650  isarchiofld  32404  sqsscirc2  32827  cnre2csqlem  32828  xrge0iifiso  32853  sigaclci  33068  omssubadd  33237  eulerpartlemb  33305  ballotlemimin  33442  ballotlem7  33472  fineqvac  34035  subgrwlk  34061  cusgracyclt3v  34085  cvmlift2lem12  34243  fmlasucdisj  34328  dfon2lem8  34700  segconeq  34920  ifscgr  34954  brofs2  34987  brifs2  34988  endofsegid  34995  dissneqlem  36159  rdgellim  36195  fvineqsneq  36231  tan2h  36418  matunitlindflem2  36423  poimirlem31  36457  poimir  36459  fzmul  36547  fdc  36551  incsequz2  36555  sstotbnd2  36580  sstotbnd3  36582  totbndbnd  36595  isexid2  36661  ispridl2  36844  mpobi123f  36968  disjlem18  37608  disjdmqsss  37610  riotasvd  37764  lsator0sp  37809  lssatle  37823  lshpset2N  37927  lkrlspeqN  37979  omllaw2N  38052  cmtbr3N  38062  lecmtN  38064  cvlcvr1  38147  cvrval4N  38223  cvrat3  38251  3noncolr2  38258  4noncolr3  38262  3dimlem3  38270  3dimlem3OLDN  38271  3dimlem4  38273  3dimlem4OLDN  38274  llncvrlpln  38367  lplncvrlvol  38425  snatpsubN  38559  linepsubN  38561  pmapjat1  38662  pclfinclN  38759  pl42N  38792  ltrneq2  38957  cdleme7aa  39051  cdleme18d  39104  cdleme21b  39135  trlord  39378  trlcoat  39532  dochkrshp  40195  lcfl8  40311  mulgt0con1dlem  41274  irrapxlem2  41494  pell14qrdich  41540  monotoddzz  41615  pw2f1ocnv  41709  iocinico  41894  ordnexbtwnsuc  41950  tfsconcat0i  42028  naddwordnexlem4  42085  harval3  42222  sbcim2g  43232  stoweidlem62  44713  elfzelfzlble  45964  1arymaptf1  47230  2arymaptf1  47241  eenglngeehlnmlem2  47326  mpbiran3d  47384  opnneil  47444