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  3794  opeldmd  5873  elreldm  5902  predtrss  6298  ordtr2  6380  ssimaex  6949  fliftfun  7290  isopolem  7323  isosolem  7325  ordsucss  7796  f1oweALT  7954  fnse  8115  soseq  8141  brtpos  8217  issmo2  8321  seqomlem1  8421  omcl  8503  oecl  8504  oawordeulem  8521  oaass  8528  omordi  8533  omord  8535  odi  8546  oen0  8553  oeordi  8554  oeordsuc  8561  nnmcl  8579  nnecl  8580  nnmordi  8598  nnmord  8599  nnmwordri  8603  nnaordex  8605  swoord1  8706  ecopovtrn  8796  f1domg  8946  pw2f1olem  9050  domtriord  9093  mapen  9111  mapxpen  9113  mapunen  9116  nndomog  9183  onomeneq  9184  inficl  9383  supmo  9410  infmo  9455  inf3lem6  9593  cantnflem1  9649  tcmin  9701  tcrank  9844  cardne  9925  cardlim  9932  cardsdomel  9934  carduni  9941  alephord  10035  cardinfima  10057  dfac5lem4  10086  dfac5lem4OLD  10088  infdif2  10169  cofsmo  10229  cfcoflem  10232  infpssrlem4  10266  infpssrlem5  10267  fin4en1  10269  isfin2-2  10279  enfin2i  10281  fin23lem27  10288  isf32lem12  10324  isf34lem6  10340  domtriomlem  10402  cardmin  10524  fpwwe2lem11  10601  inar1  10735  gruiun  10759  ltsonq  10929  prub  10954  reclem3pr  11009  mulcmpblnr  11031  mulgt0sr  11065  axpre-sup  11129  leltadd  11669  infm3  12149  peano5nni  12196  zextle  12614  prime  12622  uzin  12840  ublbneg  12899  zbtwnre  12912  mul2lt0bi  13066  xrre2  13137  xralrple  13172  xmulneg1  13236  supxrbnd  13295  supxrgtmnf  13296  fzrevral  13580  flge  13774  ceile  13818  modadd1  13877  modmul1  13896  modsumfzodifsn  13916  seqcl2  13992  facdiv  14259  hashss  14381  hash2exprb  14443  elfzelfzccat  14552  repswswrd  14756  cshf1  14782  cshwcsh2id  14801  rlim2lt  15470  rlim3  15471  o1lo1  15510  climshftlem  15547  o1co  15559  o1of2  15586  isercolllem2  15639  isercoll  15641  caucvgrlem2  15648  climcndslem2  15823  sqrt2irr  16224  dvds2lem  16245  dvdsle  16287  dvdsfac  16303  ltoddhalfle  16338  divalglem0  16370  ndvdsadd  16387  bitsinv1lem  16418  sadcaddlem  16434  dvdslegcd  16481  bezoutlem2  16517  bezoutlem4  16519  gcdzeq  16529  algcvga  16556  rpdvds  16637  cncongr1  16644  cncongr2  16645  prmind2  16662  isprm6  16691  rpexp  16699  eulerthlem2  16759  pclem  16816  pceulem  16823  pc2dvds  16857  fldivp1  16875  infpnlem1  16888  prmunb  16892  mrieqv2d  17607  plttr  18308  clatl  18474  issubg4  19084  gexdvds  19521  pgpssslw  19551  sylow2alem2  19555  efgs1b  19673  efgsfo  19676  imasabl  19813  lspindpi  21049  psgnodpm  21504  psgndif  21518  obselocv  21644  pf1ind  22249  mdetunilem9  22514  fiinbas  22846  bastg  22860  tgcl  22863  opnssneib  23009  clslp  23042  tgcnp  23147  iscnp4  23157  cncls2  23167  cncls  23168  cnntr  23169  cnpresti  23182  lmss  23192  lmcnp  23198  cmpsub  23294  tgcmp  23295  dfconn2  23313  t1connperf  23330  1stcfb  23339  1stcrest  23347  kgenss  23437  llycmpkgen2  23444  txdis  23526  qtoptop2  23593  kqt0lem  23630  isr0  23631  regr1lem2  23634  cmphaushmeo  23694  fbun  23734  ssfg  23766  fgtr  23784  ufildr  23825  cnpflf  23895  fclsnei  23913  flimfnfcls  23922  fclscmp  23924  ufilcmp  23926  cnpfcf  23935  alexsublem  23938  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem3  23948  tgphaus  24011  tgpt1  24012  tsmsres  24038  imasdsf1olem  24268  xblss2ps  24296  xblss2  24297  blsscls2  24399  metequiv2  24405  stdbdxmet  24410  nmoi  24623  reconn  24724  mulc1cncf  24805  cncfco  24807  iccpnfhmeo  24850  xrhmeo  24851  evth  24865  pi1grplem  24956  fgcfil  25178  ivthlem2  25360  ivthlem3  25361  ovolicc2lem4  25428  voliunlem1  25458  ioombl1lem4  25469  itg2gt0  25668  limcco  25801  lhop1  25926  tdeglem4  25972  plypf1  26124  coeeulem  26136  coeidlem  26149  coeid3  26152  plymul0or  26195  dvnply2  26202  plydivex  26212  vieta1lem2  26226  plyexmo  26228  aaliou3lem2  26258  ulmss  26313  ulmdvlem3  26318  iblulm  26323  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  logcnlem5  26562  dcubic  26763  amgm  26908  isnsqf  27052  mumullem2  27097  chtublem  27129  chtub  27130  fsumvma2  27132  vmasum  27134  dchrfi  27173  bposlem1  27202  bposlem3  27204  bposlem7  27208  lgsdir  27250  lgsquadlem2  27299  2sqlem8a  27343  2sqlem10  27346  dchrisum0flb  27428  pntpbnd1  27504  pntlemf  27523  pntlem3  27527  peano5uzs  28299  axeuclid  28897  uspgrushgr  29111  uspgrupgr  29112  usgruspgr  29114  usgr2pth  29701  crctcshwlkn0lem5  29751  wwlksnext  29830  wwlksnextsurj  29837  clwwlkccatlem  29925  clwlkclwwlkf  29944  clwwisshclwwslemlem  29949  lnon0  30734  normpyc  31082  ocsh  31219  ocorth  31227  ococss  31229  shsel2  31258  hsupss  31277  pjhth  31329  shlub  31350  cm2j  31556  lnfncnbd  31993  riesz1  32001  rnbra  32043  leopadd  32068  leopmuli  32069  hstles  32167  stge1i  32174  stle0i  32175  dmdbr5  32244  ssmd2  32248  superpos  32290  chcv1  32291  atoml2i  32319  chirredlem2  32327  atcvat3i  32332  mdsymlem5  32343  mdsymlem6  32344  sumdmdii  32351  sumdmdlem2  32355  isarchiofld  33302  sqsscirc2  33906  cnre2csqlem  33907  xrge0iifiso  33932  sigaclci  34129  omssubadd  34298  eulerpartlemb  34366  ballotlemimin  34504  ballotlem7  34534  fineqvac  35094  vonf1owev  35102  subgrwlk  35126  cusgracyclt3v  35150  cvmlift2lem12  35308  fmlasucdisj  35393  dfon2lem8  35785  segconeq  36005  ifscgr  36039  brofs2  36072  brifs2  36073  endofsegid  36080  dissneqlem  37335  rdgellim  37371  fvineqsneq  37407  tan2h  37613  matunitlindflem2  37618  poimirlem31  37652  poimir  37654  fzmul  37742  fdc  37746  incsequz2  37750  sstotbnd2  37775  sstotbnd3  37777  totbndbnd  37790  isexid2  37856  ispridl2  38039  mpobi123f  38163  disjlem18  38799  disjdmqsss  38801  riotasvd  38956  lsator0sp  39001  lssatle  39015  lshpset2N  39119  lkrlspeqN  39171  omllaw2N  39244  cmtbr3N  39254  lecmtN  39256  cvlcvr1  39339  cvrval4N  39415  cvrat3  39443  3noncolr2  39450  4noncolr3  39454  3dimlem3  39462  3dimlem3OLDN  39463  3dimlem4  39465  3dimlem4OLDN  39466  llncvrlpln  39559  lplncvrlvol  39617  snatpsubN  39751  linepsubN  39753  pmapjat1  39854  pclfinclN  39951  pl42N  39984  ltrneq2  40149  cdleme7aa  40243  cdleme18d  40296  cdleme21b  40327  trlord  40570  trlcoat  40724  dochkrshp  41387  lcfl8  41503  mulgt0con1dlem  42464  irrapxlem2  42818  pell14qrdich  42864  monotoddzz  42939  pw2f1ocnv  43033  iocinico  43208  ordnexbtwnsuc  43263  tfsconcat0i  43341  naddwordnexlem4  43397  harval3  43534  sbcim2g  44535  stoweidlem62  46067  elfzelfzlble  47326  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  1arymaptf1  48635  2arymaptf1  48646  eenglngeehlnmlem2  48731  mpbiran3d  48789  opnneil  48902