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  3776  opeldmd  5853  elreldm  5882  predtrss  6277  ordtr2  6359  ssimaex  6916  fliftfun  7255  isopolem  7288  isosolem  7290  ordsucss  7757  f1oweALT  7913  fnse  8072  soseq  8098  brtpos  8174  issmo2  8278  seqomlem1  8378  omcl  8460  oecl  8461  oawordeulem  8478  oaass  8485  omordi  8490  omord  8492  odi  8503  oen0  8510  oeordi  8511  oeordsuc  8518  nnmcl  8536  nnecl  8537  nnmordi  8555  nnmord  8556  nnmwordri  8560  nnaordex  8562  swoord1  8663  ecopovtrn  8753  f1domg  8903  pw2f1olem  9004  domtriord  9046  mapen  9064  mapxpen  9066  mapunen  9069  nndomog  9132  onomeneq  9133  inficl  9319  supmo  9346  infmo  9391  inf3lem6  9533  cantnflem1  9589  tcmin  9639  tcrank  9787  cardne  9868  cardlim  9875  cardsdomel  9877  carduni  9884  alephord  9976  cardinfima  9998  dfac5lem4  10027  dfac5lem4OLD  10029  infdif2  10110  cofsmo  10170  cfcoflem  10173  infpssrlem4  10207  infpssrlem5  10208  fin4en1  10210  isfin2-2  10220  enfin2i  10222  fin23lem27  10229  isf32lem12  10265  isf34lem6  10281  domtriomlem  10343  cardmin  10465  fpwwe2lem11  10542  inar1  10676  gruiun  10700  ltsonq  10870  prub  10895  reclem3pr  10950  mulcmpblnr  10972  mulgt0sr  11006  axpre-sup  11070  leltadd  11611  infm3  12091  peano5nni  12138  zextle  12556  prime  12564  uzin  12782  ublbneg  12841  zbtwnre  12854  mul2lt0bi  13008  xrre2  13079  xralrple  13114  xmulneg1  13178  supxrbnd  13237  supxrgtmnf  13238  fzrevral  13522  flge  13719  ceile  13763  modadd1  13822  modmul1  13841  modsumfzodifsn  13861  seqcl2  13937  facdiv  14204  hashss  14326  hash2exprb  14388  elfzelfzccat  14497  repswswrd  14701  cshf1  14727  cshwcsh2id  14745  rlim2lt  15414  rlim3  15415  o1lo1  15454  climshftlem  15491  o1co  15503  o1of2  15530  isercolllem2  15583  isercoll  15585  caucvgrlem2  15592  climcndslem2  15767  sqrt2irr  16168  dvds2lem  16189  dvdsle  16231  dvdsfac  16247  ltoddhalfle  16282  divalglem0  16314  ndvdsadd  16331  bitsinv1lem  16362  sadcaddlem  16378  dvdslegcd  16425  bezoutlem2  16461  bezoutlem4  16463  gcdzeq  16473  algcvga  16500  rpdvds  16581  cncongr1  16588  cncongr2  16589  prmind2  16606  isprm6  16635  rpexp  16643  eulerthlem2  16703  pclem  16760  pceulem  16767  pc2dvds  16801  fldivp1  16819  infpnlem1  16832  prmunb  16836  mrieqv2d  17555  plttr  18256  clatl  18424  issubg4  19068  gexdvds  19506  pgpssslw  19536  sylow2alem2  19540  efgs1b  19658  efgsfo  19661  imasabl  19798  lspindpi  21079  psgnodpm  21535  psgndif  21549  obselocv  21675  pf1ind  22280  mdetunilem9  22545  fiinbas  22877  bastg  22891  tgcl  22894  opnssneib  23040  clslp  23073  tgcnp  23178  iscnp4  23188  cncls2  23198  cncls  23199  cnntr  23200  cnpresti  23213  lmss  23223  lmcnp  23229  cmpsub  23325  tgcmp  23326  dfconn2  23344  t1connperf  23361  1stcfb  23370  1stcrest  23378  kgenss  23468  llycmpkgen2  23475  txdis  23557  qtoptop2  23624  kqt0lem  23661  isr0  23662  regr1lem2  23665  cmphaushmeo  23725  fbun  23765  ssfg  23797  fgtr  23815  ufildr  23856  cnpflf  23926  fclsnei  23944  flimfnfcls  23953  fclscmp  23955  ufilcmp  23957  cnpfcf  23966  alexsublem  23969  alexsubALTlem3  23974  alexsubALTlem4  23975  ptcmplem3  23979  tgphaus  24042  tgpt1  24043  tsmsres  24069  imasdsf1olem  24298  xblss2ps  24326  xblss2  24327  blsscls2  24429  metequiv2  24435  stdbdxmet  24440  nmoi  24653  reconn  24754  mulc1cncf  24835  cncfco  24837  iccpnfhmeo  24880  xrhmeo  24881  evth  24895  pi1grplem  24986  fgcfil  25208  ivthlem2  25390  ivthlem3  25391  ovolicc2lem4  25458  voliunlem1  25488  ioombl1lem4  25499  itg2gt0  25698  limcco  25831  lhop1  25956  tdeglem4  26002  plypf1  26154  coeeulem  26166  coeidlem  26179  coeid3  26182  plymul0or  26225  dvnply2  26232  plydivex  26242  vieta1lem2  26256  plyexmo  26258  aaliou3lem2  26288  ulmss  26343  ulmdvlem3  26348  iblulm  26353  sincosq2sgn  26445  sincosq3sgn  26446  sincosq4sgn  26447  logcnlem5  26592  dcubic  26793  amgm  26938  isnsqf  27082  mumullem2  27127  chtublem  27159  chtub  27160  fsumvma2  27162  vmasum  27164  dchrfi  27203  bposlem1  27232  bposlem3  27234  bposlem7  27238  lgsdir  27280  lgsquadlem2  27329  2sqlem8a  27373  2sqlem10  27376  dchrisum0flb  27458  pntpbnd1  27534  pntlemf  27553  pntlem3  27557  peano5uzs  28338  axeuclid  28952  uspgrushgr  29166  uspgrupgr  29167  usgruspgr  29169  usgr2pth  29753  crctcshwlkn0lem5  29803  wwlksnext  29882  wwlksnextsurj  29889  clwwlkccatlem  29980  clwlkclwwlkf  29999  clwwisshclwwslemlem  30004  lnon0  30789  normpyc  31137  ocsh  31274  ocorth  31282  ococss  31284  shsel2  31313  hsupss  31332  pjhth  31384  shlub  31405  cm2j  31611  lnfncnbd  32048  riesz1  32056  rnbra  32098  leopadd  32123  leopmuli  32124  hstles  32222  stge1i  32229  stle0i  32230  dmdbr5  32299  ssmd2  32303  superpos  32345  chcv1  32346  atoml2i  32374  chirredlem2  32382  atcvat3i  32387  mdsymlem5  32398  mdsymlem6  32399  sumdmdii  32406  sumdmdlem2  32410  isarchiofld  33179  sqsscirc2  33933  cnre2csqlem  33934  xrge0iifiso  33959  sigaclci  34156  omssubadd  34324  eulerpartlemb  34392  ballotlemimin  34530  ballotlem7  34560  fineqvac  35150  vonf1owev  35163  subgrwlk  35187  cusgracyclt3v  35211  cvmlift2lem12  35369  fmlasucdisj  35454  dfon2lem8  35843  segconeq  36065  ifscgr  36099  brofs2  36132  brifs2  36133  endofsegid  36140  dissneqlem  37395  rdgellim  37431  fvineqsneq  37467  tan2h  37662  matunitlindflem2  37667  poimirlem31  37701  poimir  37703  fzmul  37791  fdc  37795  incsequz2  37799  sstotbnd2  37824  sstotbnd3  37826  totbndbnd  37839  isexid2  37905  ispridl2  38088  mpobi123f  38212  disjlem18  38908  disjdmqsss  38910  riotasvd  39065  lsator0sp  39110  lssatle  39124  lshpset2N  39228  lkrlspeqN  39280  omllaw2N  39353  cmtbr3N  39363  lecmtN  39365  cvlcvr1  39448  cvrval4N  39523  cvrat3  39551  3noncolr2  39558  4noncolr3  39562  3dimlem3  39570  3dimlem3OLDN  39571  3dimlem4  39573  3dimlem4OLDN  39574  llncvrlpln  39667  lplncvrlvol  39725  snatpsubN  39859  linepsubN  39861  pmapjat1  39962  pclfinclN  40059  pl42N  40092  ltrneq2  40257  cdleme7aa  40351  cdleme18d  40404  cdleme21b  40435  trlord  40678  trlcoat  40832  dochkrshp  41495  lcfl8  41611  mulgt0con1dlem  42577  irrapxlem2  42930  pell14qrdich  42976  monotoddzz  43050  pw2f1ocnv  43144  iocinico  43319  ordnexbtwnsuc  43374  tfsconcat0i  43452  naddwordnexlem4  43508  harval3  43645  sbcim2g  44645  stoweidlem62  46174  elfzelfzlble  47435  pgnbgreunbgrlem1  48227  pgnbgreunbgrlem4  48233  1arymaptf1  48757  2arymaptf1  48768  eenglngeehlnmlem2  48853  mpbiran3d  48911  opnneil  49024