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  3767  opeldmd  5862  elreldm  5891  predtrss  6287  ordtr2  6369  ssimaex  6926  fliftfun  7267  isopolem  7300  isosolem  7302  ordsucss  7769  f1oweALT  7925  fnse  8083  soseq  8109  brtpos  8185  issmo2  8289  seqomlem1  8389  omcl  8471  oecl  8472  oawordeulem  8489  oaass  8496  omordi  8501  omord  8503  odi  8514  oen0  8522  oeordi  8523  oeordsuc  8530  nnmcl  8548  nnecl  8549  nnmordi  8567  nnmord  8568  nnmwordri  8572  nnaordex  8574  swoord1  8676  ecopovtrn  8767  f1domg  8918  pw2f1olem  9019  domtriord  9061  mapen  9079  mapxpen  9081  mapunen  9084  nndomog  9147  onomeneq  9148  inficl  9338  supmo  9365  infmo  9410  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  11634  infm3  12115  peano5nni  12177  zextle  12602  prime  12610  uzin  12824  ublbneg  12883  zbtwnre  12896  mul2lt0bi  13050  xrre2  13122  xralrple  13157  xmulneg1  13221  supxrbnd  13280  supxrgtmnf  13281  fzrevral  13566  flge  13764  ceile  13808  modadd1  13867  modmul1  13886  modsumfzodifsn  13906  seqcl2  13982  facdiv  14249  hashss  14371  hash2exprb  14433  elfzelfzccat  14542  repswswrd  14746  cshf1  14772  cshwcsh2id  14790  rlim2lt  15459  rlim3  15460  o1lo1  15499  climshftlem  15536  o1co  15548  o1of2  15575  isercolllem2  15628  isercoll  15630  caucvgrlem2  15637  climcndslem2  15815  sqrt2irr  16216  dvds2lem  16237  dvdsle  16279  dvdsfac  16295  ltoddhalfle  16330  divalglem0  16362  ndvdsadd  16379  bitsinv1lem  16410  sadcaddlem  16426  dvdslegcd  16473  bezoutlem2  16509  bezoutlem4  16511  gcdzeq  16521  algcvga  16548  rpdvds  16629  cncongr1  16636  cncongr2  16637  prmind2  16654  isprm6  16684  rpexp  16692  eulerthlem2  16752  pclem  16809  pceulem  16816  pc2dvds  16850  fldivp1  16868  infpnlem1  16881  prmunb  16885  mrieqv2d  17605  plttr  18306  clatl  18474  issubg4  19121  gexdvds  19559  pgpssslw  19589  sylow2alem2  19593  efgs1b  19711  efgsfo  19714  imasabl  19851  lspindpi  21130  psgnodpm  21568  psgndif  21582  obselocv  21708  pf1ind  22320  mdetunilem9  22585  fiinbas  22917  bastg  22931  tgcl  22934  opnssneib  23080  clslp  23113  tgcnp  23218  iscnp4  23228  cncls2  23238  cncls  23239  cnntr  23240  cnpresti  23253  lmss  23263  lmcnp  23269  cmpsub  23365  tgcmp  23366  dfconn2  23384  t1connperf  23401  1stcfb  23410  1stcrest  23418  kgenss  23508  llycmpkgen2  23515  txdis  23597  qtoptop2  23664  kqt0lem  23701  isr0  23702  regr1lem2  23705  cmphaushmeo  23765  fbun  23805  ssfg  23837  fgtr  23855  ufildr  23896  cnpflf  23966  fclsnei  23984  flimfnfcls  23993  fclscmp  23995  ufilcmp  23997  cnpfcf  24006  alexsublem  24009  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem3  24019  tgphaus  24082  tgpt1  24083  tsmsres  24109  imasdsf1olem  24338  xblss2ps  24366  xblss2  24367  blsscls2  24469  metequiv2  24475  stdbdxmet  24480  nmoi  24693  reconn  24794  mulc1cncf  24872  cncfco  24874  iccpnfhmeo  24912  xrhmeo  24913  evth  24926  pi1grplem  25016  fgcfil  25238  ivthlem2  25419  ivthlem3  25420  ovolicc2lem4  25487  voliunlem1  25517  ioombl1lem4  25528  itg2gt0  25727  limcco  25860  lhop1  25981  tdeglem4  26025  plypf1  26177  coeeulem  26189  coeidlem  26202  coeid3  26205  plymul0or  26247  dvnply2  26253  plydivex  26263  vieta1lem2  26277  plyexmo  26279  aaliou3lem2  26309  ulmss  26362  ulmdvlem3  26367  iblulm  26372  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  logcnlem5  26610  dcubic  26810  amgm  26954  isnsqf  27098  mumullem2  27143  chtublem  27174  chtub  27175  fsumvma2  27177  vmasum  27179  dchrfi  27218  bposlem1  27247  bposlem3  27249  bposlem7  27253  lgsdir  27295  lgsquadlem2  27344  2sqlem8a  27388  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  pntlemf  27568  pntlem3  27572  addonbday  28271  peano5uzs  28396  axeuclid  29032  uspgrushgr  29246  uspgrupgr  29247  usgruspgr  29249  usgr2pth  29832  crctcshwlkn0lem5  29882  wwlksnext  29961  wwlksnextsurj  29968  clwwlkccatlem  30059  clwlkclwwlkf  30078  clwwisshclwwslemlem  30083  lnon0  30869  normpyc  31217  ocsh  31354  ocorth  31362  ococss  31364  shsel2  31393  hsupss  31412  pjhth  31464  shlub  31485  cm2j  31691  lnfncnbd  32128  riesz1  32136  rnbra  32178  leopadd  32203  leopmuli  32204  hstles  32302  stge1i  32309  stle0i  32310  dmdbr5  32379  ssmd2  32383  superpos  32425  chcv1  32426  atoml2i  32454  chirredlem2  32462  atcvat3i  32467  mdsymlem5  32478  mdsymlem6  32479  sumdmdii  32486  sumdmdlem2  32490  isarchiofld  33260  sqsscirc2  34053  cnre2csqlem  34054  xrge0iifiso  34079  sigaclci  34276  omssubadd  34444  eulerpartlemb  34512  ballotlemimin  34650  ballotlem7  34680  fineqvac  35260  fineqvinfep  35269  vonf1owev  35290  subgrwlk  35314  cusgracyclt3v  35338  cvmlift2lem12  35496  fmlasucdisj  35581  dfon2lem8  35970  segconeq  36192  ifscgr  36226  brofs2  36259  brifs2  36260  endofsegid  36267  dissneqlem  37656  rdgellim  37692  fvineqsneq  37728  tan2h  37933  matunitlindflem2  37938  poimirlem31  37972  poimir  37974  fzmul  38062  fdc  38066  incsequz2  38070  sstotbnd2  38095  sstotbnd3  38097  totbndbnd  38110  isexid2  38176  ispridl2  38359  mpobi123f  38483  disjlem18  39224  disjdmqsss  39226  eldisjs6  39261  riotasvd  39402  lsator0sp  39447  lssatle  39461  lshpset2N  39565  lkrlspeqN  39617  omllaw2N  39690  cmtbr3N  39700  lecmtN  39702  cvlcvr1  39785  cvrval4N  39860  cvrat3  39888  3noncolr2  39895  4noncolr3  39899  3dimlem3  39907  3dimlem3OLDN  39908  3dimlem4  39910  3dimlem4OLDN  39911  llncvrlpln  40004  lplncvrlvol  40062  snatpsubN  40196  linepsubN  40198  pmapjat1  40299  pclfinclN  40396  pl42N  40429  ltrneq2  40594  cdleme7aa  40688  cdleme18d  40741  cdleme21b  40772  trlord  41015  trlcoat  41169  dochkrshp  41832  lcfl8  41948  mulgt0con1dlem  42914  irrapxlem2  43251  pell14qrdich  43297  monotoddzz  43371  pw2f1ocnv  43465  iocinico  43640  ordnexbtwnsuc  43695  tfsconcat0i  43773  naddwordnexlem4  43829  harval3  43965  sbcim2g  44965  stoweidlem62  46490  elfzelfzlble  47763  pgnbgreunbgrlem1  48583  pgnbgreunbgrlem4  48589  1arymaptf1  49112  2arymaptf1  49123  eenglngeehlnmlem2  49208  mpbiran3d  49266  opnneil  49379