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  3791  opeldmd  5870  elreldm  5899  predtrss  6295  ordtr2  6377  ssimaex  6946  fliftfun  7287  isopolem  7320  isosolem  7322  ordsucss  7793  f1oweALT  7951  fnse  8112  soseq  8138  brtpos  8214  issmo2  8318  seqomlem1  8418  omcl  8500  oecl  8501  oawordeulem  8518  oaass  8525  omordi  8530  omord  8532  odi  8543  oen0  8550  oeordi  8551  oeordsuc  8558  nnmcl  8576  nnecl  8577  nnmordi  8595  nnmord  8596  nnmwordri  8600  nnaordex  8602  swoord1  8703  ecopovtrn  8793  f1domg  8943  pw2f1olem  9045  domtriord  9087  mapen  9105  mapxpen  9107  mapunen  9110  nndomog  9177  onomeneq  9178  inficl  9376  supmo  9403  infmo  9448  inf3lem6  9586  cantnflem1  9642  tcmin  9694  tcrank  9837  cardne  9918  cardlim  9925  cardsdomel  9927  carduni  9934  alephord  10028  cardinfima  10050  dfac5lem4  10079  dfac5lem4OLD  10081  infdif2  10162  cofsmo  10222  cfcoflem  10225  infpssrlem4  10259  infpssrlem5  10260  fin4en1  10262  isfin2-2  10272  enfin2i  10274  fin23lem27  10281  isf32lem12  10317  isf34lem6  10333  domtriomlem  10395  cardmin  10517  fpwwe2lem11  10594  inar1  10728  gruiun  10752  ltsonq  10922  prub  10947  reclem3pr  11002  mulcmpblnr  11024  mulgt0sr  11058  axpre-sup  11122  leltadd  11662  infm3  12142  peano5nni  12189  zextle  12607  prime  12615  uzin  12833  ublbneg  12892  zbtwnre  12905  mul2lt0bi  13059  xrre2  13130  xralrple  13165  xmulneg1  13229  supxrbnd  13288  supxrgtmnf  13289  fzrevral  13573  flge  13767  ceile  13811  modadd1  13870  modmul1  13889  modsumfzodifsn  13909  seqcl2  13985  facdiv  14252  hashss  14374  hash2exprb  14436  elfzelfzccat  14545  repswswrd  14749  cshf1  14775  cshwcsh2id  14794  rlim2lt  15463  rlim3  15464  o1lo1  15503  climshftlem  15540  o1co  15552  o1of2  15579  isercolllem2  15632  isercoll  15634  caucvgrlem2  15641  climcndslem2  15816  sqrt2irr  16217  dvds2lem  16238  dvdsle  16280  dvdsfac  16296  ltoddhalfle  16331  divalglem0  16363  ndvdsadd  16380  bitsinv1lem  16411  sadcaddlem  16427  dvdslegcd  16474  bezoutlem2  16510  bezoutlem4  16512  gcdzeq  16522  algcvga  16549  rpdvds  16630  cncongr1  16637  cncongr2  16638  prmind2  16655  isprm6  16684  rpexp  16692  eulerthlem2  16752  pclem  16809  pceulem  16816  pc2dvds  16850  fldivp1  16868  infpnlem1  16881  prmunb  16885  mrieqv2d  17600  plttr  18301  clatl  18467  issubg4  19077  gexdvds  19514  pgpssslw  19544  sylow2alem2  19548  efgs1b  19666  efgsfo  19669  imasabl  19806  lspindpi  21042  psgnodpm  21497  psgndif  21511  obselocv  21637  pf1ind  22242  mdetunilem9  22507  fiinbas  22839  bastg  22853  tgcl  22856  opnssneib  23002  clslp  23035  tgcnp  23140  iscnp4  23150  cncls2  23160  cncls  23161  cnntr  23162  cnpresti  23175  lmss  23185  lmcnp  23191  cmpsub  23287  tgcmp  23288  dfconn2  23306  t1connperf  23323  1stcfb  23332  1stcrest  23340  kgenss  23430  llycmpkgen2  23437  txdis  23519  qtoptop2  23586  kqt0lem  23623  isr0  23624  regr1lem2  23627  cmphaushmeo  23687  fbun  23727  ssfg  23759  fgtr  23777  ufildr  23818  cnpflf  23888  fclsnei  23906  flimfnfcls  23915  fclscmp  23917  ufilcmp  23919  cnpfcf  23928  alexsublem  23931  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem3  23941  tgphaus  24004  tgpt1  24005  tsmsres  24031  imasdsf1olem  24261  xblss2ps  24289  xblss2  24290  blsscls2  24392  metequiv2  24398  stdbdxmet  24403  nmoi  24616  reconn  24717  mulc1cncf  24798  cncfco  24800  iccpnfhmeo  24843  xrhmeo  24844  evth  24858  pi1grplem  24949  fgcfil  25171  ivthlem2  25353  ivthlem3  25354  ovolicc2lem4  25421  voliunlem1  25451  ioombl1lem4  25462  itg2gt0  25661  limcco  25794  lhop1  25919  tdeglem4  25965  plypf1  26117  coeeulem  26129  coeidlem  26142  coeid3  26145  plymul0or  26188  dvnply2  26195  plydivex  26205  vieta1lem2  26219  plyexmo  26221  aaliou3lem2  26251  ulmss  26306  ulmdvlem3  26311  iblulm  26316  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  logcnlem5  26555  dcubic  26756  amgm  26901  isnsqf  27045  mumullem2  27090  chtublem  27122  chtub  27123  fsumvma2  27125  vmasum  27127  dchrfi  27166  bposlem1  27195  bposlem3  27197  bposlem7  27201  lgsdir  27243  lgsquadlem2  27292  2sqlem8a  27336  2sqlem10  27339  dchrisum0flb  27421  pntpbnd1  27497  pntlemf  27516  pntlem3  27520  peano5uzs  28292  axeuclid  28890  uspgrushgr  29104  uspgrupgr  29105  usgruspgr  29107  usgr2pth  29694  crctcshwlkn0lem5  29744  wwlksnext  29823  wwlksnextsurj  29830  clwwlkccatlem  29918  clwlkclwwlkf  29937  clwwisshclwwslemlem  29942  lnon0  30727  normpyc  31075  ocsh  31212  ocorth  31220  ococss  31222  shsel2  31251  hsupss  31270  pjhth  31322  shlub  31343  cm2j  31549  lnfncnbd  31986  riesz1  31994  rnbra  32036  leopadd  32061  leopmuli  32062  hstles  32160  stge1i  32167  stle0i  32168  dmdbr5  32237  ssmd2  32241  superpos  32283  chcv1  32284  atoml2i  32312  chirredlem2  32320  atcvat3i  32325  mdsymlem5  32336  mdsymlem6  32337  sumdmdii  32344  sumdmdlem2  32348  isarchiofld  33295  sqsscirc2  33899  cnre2csqlem  33900  xrge0iifiso  33925  sigaclci  34122  omssubadd  34291  eulerpartlemb  34359  ballotlemimin  34497  ballotlem7  34527  fineqvac  35087  vonf1owev  35095  subgrwlk  35119  cusgracyclt3v  35143  cvmlift2lem12  35301  fmlasucdisj  35386  dfon2lem8  35778  segconeq  35998  ifscgr  36032  brofs2  36065  brifs2  36066  endofsegid  36073  dissneqlem  37328  rdgellim  37364  fvineqsneq  37400  tan2h  37606  matunitlindflem2  37611  poimirlem31  37645  poimir  37647  fzmul  37735  fdc  37739  incsequz2  37743  sstotbnd2  37768  sstotbnd3  37770  totbndbnd  37783  isexid2  37849  ispridl2  38032  mpobi123f  38156  disjlem18  38792  disjdmqsss  38794  riotasvd  38949  lsator0sp  38994  lssatle  39008  lshpset2N  39112  lkrlspeqN  39164  omllaw2N  39237  cmtbr3N  39247  lecmtN  39249  cvlcvr1  39332  cvrval4N  39408  cvrat3  39436  3noncolr2  39443  4noncolr3  39447  3dimlem3  39455  3dimlem3OLDN  39456  3dimlem4  39458  3dimlem4OLDN  39459  llncvrlpln  39552  lplncvrlvol  39610  snatpsubN  39744  linepsubN  39746  pmapjat1  39847  pclfinclN  39944  pl42N  39977  ltrneq2  40142  cdleme7aa  40236  cdleme18d  40289  cdleme21b  40320  trlord  40563  trlcoat  40717  dochkrshp  41380  lcfl8  41496  mulgt0con1dlem  42457  irrapxlem2  42811  pell14qrdich  42857  monotoddzz  42932  pw2f1ocnv  43026  iocinico  43201  ordnexbtwnsuc  43256  tfsconcat0i  43334  naddwordnexlem4  43390  harval3  43527  sbcim2g  44528  stoweidlem62  46060  elfzelfzlble  47322  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  1arymaptf1  48631  2arymaptf1  48642  eenglngeehlnmlem2  48727  mpbiran3d  48785  opnneil  48898