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  3803  opeldmd  5886  elreldm  5915  predtrss  6311  ordtr2  6397  ssimaex  6963  fliftfun  7304  isopolem  7337  isosolem  7339  ordsucss  7810  f1oweALT  7969  fnse  8130  soseq  8156  brtpos  8232  issmo2  8361  seqomlem1  8462  omcl  8546  oecl  8547  oawordeulem  8564  oaass  8571  omordi  8576  omord  8578  odi  8589  oen0  8596  oeordi  8597  oeordsuc  8604  nnmcl  8622  nnecl  8623  nnmordi  8641  nnmord  8642  nnmwordri  8646  nnaordex  8648  swoord1  8749  ecopovtrn  8832  f1domg  8984  pw2f1olem  9088  domtriord  9135  mapen  9153  mapxpen  9155  mapunen  9158  nndomog  9225  nndomogOLD  9233  onomeneq  9235  inficl  9435  supmo  9462  infmo  9507  inf3lem6  9645  cantnflem1  9701  tcmin  9753  tcrank  9896  cardne  9977  cardlim  9984  cardsdomel  9986  carduni  9993  alephord  10087  cardinfima  10109  dfac5lem4  10138  dfac5lem4OLD  10140  infdif2  10221  cofsmo  10281  cfcoflem  10284  infpssrlem4  10318  infpssrlem5  10319  fin4en1  10321  isfin2-2  10331  enfin2i  10333  fin23lem27  10340  isf32lem12  10376  isf34lem6  10392  domtriomlem  10454  cardmin  10576  fpwwe2lem11  10653  inar1  10787  gruiun  10811  ltsonq  10981  prub  11006  reclem3pr  11061  mulcmpblnr  11083  mulgt0sr  11117  axpre-sup  11181  leltadd  11719  infm3  12199  peano5nni  12241  zextle  12664  prime  12672  uzin  12890  ublbneg  12947  zbtwnre  12960  mul2lt0bi  13113  xrre2  13184  xralrple  13219  xmulneg1  13283  supxrbnd  13342  supxrgtmnf  13343  fzrevral  13627  flge  13820  ceile  13864  modadd1  13923  modmul1  13940  modsumfzodifsn  13960  seqcl2  14036  facdiv  14303  hashss  14425  hash2exprb  14487  elfzelfzccat  14596  repswswrd  14800  cshf1  14826  cshwcsh2id  14845  rlim2lt  15511  rlim3  15512  o1lo1  15551  climshftlem  15588  o1co  15600  o1of2  15627  isercolllem2  15680  isercoll  15682  caucvgrlem2  15689  climcndslem2  15864  sqrt2irr  16265  dvds2lem  16286  dvdsle  16327  dvdsfac  16343  ltoddhalfle  16378  divalglem0  16410  ndvdsadd  16427  bitsinv1lem  16458  sadcaddlem  16474  dvdslegcd  16521  bezoutlem2  16557  bezoutlem4  16559  gcdzeq  16569  algcvga  16596  rpdvds  16677  cncongr1  16684  cncongr2  16685  prmind2  16702  isprm6  16731  rpexp  16739  eulerthlem2  16799  pclem  16856  pceulem  16863  pc2dvds  16897  fldivp1  16915  infpnlem1  16928  prmunb  16932  mrieqv2d  17649  plttr  18350  clatl  18516  issubg4  19126  gexdvds  19563  pgpssslw  19593  sylow2alem2  19597  efgs1b  19715  efgsfo  19718  imasabl  19855  lspindpi  21091  psgnodpm  21546  psgndif  21560  obselocv  21686  pf1ind  22291  mdetunilem9  22556  fiinbas  22888  bastg  22902  tgcl  22905  opnssneib  23051  clslp  23084  tgcnp  23189  iscnp4  23199  cncls2  23209  cncls  23210  cnntr  23211  cnpresti  23224  lmss  23234  lmcnp  23240  cmpsub  23336  tgcmp  23337  dfconn2  23355  t1connperf  23372  1stcfb  23381  1stcrest  23389  kgenss  23479  llycmpkgen2  23486  txdis  23568  qtoptop2  23635  kqt0lem  23672  isr0  23673  regr1lem2  23676  cmphaushmeo  23736  fbun  23776  ssfg  23808  fgtr  23826  ufildr  23867  cnpflf  23937  fclsnei  23955  flimfnfcls  23964  fclscmp  23966  ufilcmp  23968  cnpfcf  23977  alexsublem  23980  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem3  23990  tgphaus  24053  tgpt1  24054  tsmsres  24080  imasdsf1olem  24310  xblss2ps  24338  xblss2  24339  blsscls2  24441  metequiv2  24447  stdbdxmet  24452  nmoi  24665  reconn  24766  mulc1cncf  24847  cncfco  24849  iccpnfhmeo  24892  xrhmeo  24893  evth  24907  pi1grplem  24998  fgcfil  25221  ivthlem2  25403  ivthlem3  25404  ovolicc2lem4  25471  voliunlem1  25501  ioombl1lem4  25512  itg2gt0  25711  limcco  25844  lhop1  25969  tdeglem4  26015  plypf1  26167  coeeulem  26179  coeidlem  26192  coeid3  26195  plymul0or  26238  dvnply2  26245  plydivex  26255  vieta1lem2  26269  plyexmo  26271  aaliou3lem2  26301  ulmss  26356  ulmdvlem3  26361  iblulm  26366  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  logcnlem5  26605  dcubic  26806  amgm  26951  isnsqf  27095  mumullem2  27140  chtublem  27172  chtub  27173  fsumvma2  27175  vmasum  27177  dchrfi  27216  bposlem1  27245  bposlem3  27247  bposlem7  27251  lgsdir  27293  lgsquadlem2  27342  2sqlem8a  27386  2sqlem10  27389  dchrisum0flb  27471  pntpbnd1  27547  pntlemf  27566  pntlem3  27570  peano5uzs  28307  axeuclid  28888  uspgrushgr  29102  uspgrupgr  29103  usgruspgr  29105  usgr2pth  29692  crctcshwlkn0lem5  29742  wwlksnext  29821  wwlksnextsurj  29828  clwwlkccatlem  29916  clwlkclwwlkf  29935  clwwisshclwwslemlem  29940  lnon0  30725  normpyc  31073  ocsh  31210  ocorth  31218  ococss  31220  shsel2  31249  hsupss  31268  pjhth  31320  shlub  31341  cm2j  31547  lnfncnbd  31984  riesz1  31992  rnbra  32034  leopadd  32059  leopmuli  32060  hstles  32158  stge1i  32165  stle0i  32166  dmdbr5  32235  ssmd2  32239  superpos  32281  chcv1  32282  atoml2i  32310  chirredlem2  32318  atcvat3i  32323  mdsymlem5  32334  mdsymlem6  32335  sumdmdii  32342  sumdmdlem2  32346  isarchiofld  33285  sqsscirc2  33886  cnre2csqlem  33887  xrge0iifiso  33912  sigaclci  34109  omssubadd  34278  eulerpartlemb  34346  ballotlemimin  34484  ballotlem7  34514  fineqvac  35074  subgrwlk  35100  cusgracyclt3v  35124  cvmlift2lem12  35282  fmlasucdisj  35367  dfon2lem8  35754  segconeq  35974  ifscgr  36008  brofs2  36041  brifs2  36042  endofsegid  36049  dissneqlem  37304  rdgellim  37340  fvineqsneq  37376  tan2h  37582  matunitlindflem2  37587  poimirlem31  37621  poimir  37623  fzmul  37711  fdc  37715  incsequz2  37719  sstotbnd2  37744  sstotbnd3  37746  totbndbnd  37759  isexid2  37825  ispridl2  38008  mpobi123f  38132  disjlem18  38764  disjdmqsss  38766  riotasvd  38920  lsator0sp  38965  lssatle  38979  lshpset2N  39083  lkrlspeqN  39135  omllaw2N  39208  cmtbr3N  39218  lecmtN  39220  cvlcvr1  39303  cvrval4N  39379  cvrat3  39407  3noncolr2  39414  4noncolr3  39418  3dimlem3  39426  3dimlem3OLDN  39427  3dimlem4  39429  3dimlem4OLDN  39430  llncvrlpln  39523  lplncvrlvol  39581  snatpsubN  39715  linepsubN  39717  pmapjat1  39818  pclfinclN  39915  pl42N  39948  ltrneq2  40113  cdleme7aa  40207  cdleme18d  40260  cdleme21b  40291  trlord  40534  trlcoat  40688  dochkrshp  41351  lcfl8  41467  mulgt0con1dlem  42447  irrapxlem2  42793  pell14qrdich  42839  monotoddzz  42914  pw2f1ocnv  43008  iocinico  43183  ordnexbtwnsuc  43238  tfsconcat0i  43316  naddwordnexlem4  43372  harval3  43509  sbcim2g  44511  stoweidlem62  46039  elfzelfzlble  47298  1arymaptf1  48570  2arymaptf1  48581  eenglngeehlnmlem2  48666  mpbiran3d  48724  opnneil  48832