Theorem sylibrd 258

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 247	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4d  294  sbciegft  3755  opeldmd  5818  elreldm  5847  predtrss  6229  ordtr2  6314  ssimaex  6862  fliftfun  7192  isopolem  7225  isosolem  7227  ordsucss  7674  f1oweALT  7824  fnse  7983  brtpos  8060  issmo2  8189  seqomlem1  8290  omcl  8375  oecl  8376  oawordeulem  8394  oaass  8401  omordi  8406  omord  8408  odi  8419  oen0  8426  oeordi  8427  oeordsuc  8434  nnmcl  8452  nnecl  8453  nnmordi  8471  nnmord  8472  nnmwordri  8476  nnaordex  8478  swoord1  8538  ecopovtrn  8618  f1domg  8769  pw2f1olem  8872  domtriord  8919  mapen  8937  mapxpen  8939  mapunen  8942  nndomog  9008  nndomogOLD  9018  onomeneq  9020  inficl  9193  supmo  9220  infmo  9263  inf3lem6  9400  cantnflem1  9456  tcmin  9508  tcrank  9651  cardne  9732  cardlim  9739  cardsdomel  9741  carduni  9748  alephord  9840  cardinfima  9862  dfac5lem4  9891  infdif2  9975  cofsmo  10034  cfcoflem  10037  infpssrlem4  10071  infpssrlem5  10072  fin4en1  10074  isfin2-2  10084  enfin2i  10086  fin23lem27  10093  isf32lem12  10129  isf34lem6  10145  domtriomlem  10207  cardmin  10329  fpwwe2lem11  10406  inar1  10540  gruiun  10564  ltsonq  10734  prub  10759  reclem3pr  10814  mulcmpblnr  10836  mulgt0sr  10870  axpre-sup  10934  leltadd  11468  infm3  11943  peano5nni  11985  zextle  12402  prime  12410  uzin  12627  ublbneg  12682  zbtwnre  12695  mul2lt0bi  12845  xrre2  12913  xralrple  12948  xmulneg1  13012  supxrbnd  13071  supxrgtmnf  13072  fzrevral  13350  flge  13534  ceile  13578  modadd1  13637  modmul1  13653  modsumfzodifsn  13673  seqcl2  13750  facdiv  14010  hashss  14133  hash2exprb  14194  elfzelfzccat  14294  repswswrd  14506  cshf1  14532  cshwcsh2id  14550  rlim2lt  15215  rlim3  15216  o1lo1  15255  climshftlem  15292  o1co  15304  o1of2  15331  isercolllem2  15386  isercoll  15388  caucvgrlem2  15395  climcndslem2  15571  sqrt2irr  15967  dvds2lem  15987  dvdsle  16028  dvdsfac  16044  ltoddhalfle  16079  divalglem0  16111  ndvdsadd  16128  bitsinv1lem  16157  sadcaddlem  16173  dvdslegcd  16220  bezoutlem2  16257  bezoutlem4  16259  gcdzeq  16271  algcvga  16293  rpdvds  16374  cncongr1  16381  cncongr2  16382  prmind2  16399  isprm6  16428  rpexp  16436  eulerthlem2  16492  pclem  16548  pceulem  16555  pc2dvds  16589  fldivp1  16607  infpnlem1  16620  prmunb  16624  mrieqv2d  17357  plttr  18069  clatl  18235  issubg4  18783  gexdvds  19198  pgpssslw  19228  sylow2alem2  19232  efgs1b  19351  efgsfo  19354  lspindpi  20403  psgnodpm  20802  psgndif  20816  obselocv  20944  pf1ind  21530  mdetunilem9  21778  fiinbas  22111  bastg  22125  tgcl  22128  opnssneib  22275  clslp  22308  tgcnp  22413  iscnp4  22423  cncls2  22433  cncls  22434  cnntr  22435  cnpresti  22448  lmss  22458  lmcnp  22464  cmpsub  22560  tgcmp  22561  dfconn2  22579  t1connperf  22596  1stcfb  22605  1stcrest  22613  kgenss  22703  llycmpkgen2  22710  txdis  22792  qtoptop2  22859  kqt0lem  22896  isr0  22897  regr1lem2  22900  cmphaushmeo  22960  fbun  23000  ssfg  23032  fgtr  23050  ufildr  23091  cnpflf  23161  fclsnei  23179  flimfnfcls  23188  fclscmp  23190  ufilcmp  23192  cnpfcf  23201  alexsublem  23204  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem3  23214  tgphaus  23277  tgpt1  23278  tsmsres  23304  imasdsf1olem  23535  xblss2ps  23563  xblss2  23564  blsscls2  23669  metequiv2  23675  stdbdxmet  23680  nmoi  23901  reconn  24000  mulc1cncf  24077  cncfco  24079  iccpnfhmeo  24117  xrhmeo  24118  evth  24131  pi1grplem  24221  fgcfil  24444  ivthlem2  24625  ivthlem3  24626  ovolicc2lem4  24693  voliunlem1  24723  ioombl1lem4  24734  itg2gt0  24934  limcco  25066  lhop1  25187  tdeglem4  25233  tdeglem4OLD  25234  plypf1  25382  coeeulem  25394  coeidlem  25407  coeid3  25410  plymul0or  25450  dvnply2  25456  plydivex  25466  vieta1lem2  25480  plyexmo  25482  aaliou3lem2  25512  ulmss  25565  ulmdvlem3  25570  iblulm  25575  sincosq2sgn  25665  sincosq3sgn  25666  sincosq4sgn  25667  logcnlem5  25810  dcubic  26005  amgm  26149  isnsqf  26293  mumullem2  26338  chtublem  26368  chtub  26369  fsumvma2  26371  vmasum  26373  dchrfi  26412  bposlem1  26441  bposlem3  26443  bposlem7  26447  lgsdir  26489  lgsquadlem2  26538  2sqlem8a  26582  2sqlem10  26585  dchrisum0flb  26667  pntpbnd1  26743  pntlemf  26762  pntlem3  26766  axeuclid  27340  uspgrushgr  27554  uspgrupgr  27555  usgruspgr  27557  usgr2pth  28141  crctcshwlkn0lem5  28188  wwlksnext  28267  wwlksnextsurj  28274  clwwlkccatlem  28362  clwlkclwwlkf  28381  clwwisshclwwslemlem  28386  lnon0  29169  normpyc  29517  ocsh  29654  ocorth  29662  ococss  29664  shsel2  29693  hsupss  29712  pjhth  29764  shlub  29785  cm2j  29991  lnfncnbd  30428  riesz1  30436  rnbra  30478  leopadd  30503  leopmuli  30504  hstles  30602  stge1i  30609  stle0i  30610  dmdbr5  30679  ssmd2  30683  superpos  30725  chcv1  30726  atoml2i  30754  chirredlem2  30762  atcvat3i  30767  mdsymlem5  30778  mdsymlem6  30779  sumdmdii  30786  sumdmdlem2  30790  isarchiofld  31525  sqsscirc2  31868  cnre2csqlem  31869  xrge0iifiso  31894  sigaclci  32109  omssubadd  32276  eulerpartlemb  32344  ballotlemimin  32481  ballotlem7  32511  fineqvac  33075  subgrwlk  33103  cusgracyclt3v  33127  cvmlift2lem12  33285  fmlasucdisj  33370  dfon2lem8  33775  soseq  33812  segconeq  34321  ifscgr  34355  brofs2  34388  brifs2  34389  endofsegid  34396  dissneqlem  35520  rdgellim  35556  fvineqsneq  35592  tan2h  35778  matunitlindflem2  35783  poimirlem31  35817  poimir  35819  fzmul  35908  fdc  35912  incsequz2  35916  sstotbnd2  35941  sstotbnd3  35943  totbndbnd  35956  isexid2  36022  ispridl2  36205  mpobi123f  36329  riotasvd  36977  lsator0sp  37022  lssatle  37036  lshpset2N  37140  lkrlspeqN  37192  omllaw2N  37265  cmtbr3N  37275  lecmtN  37277  cvlcvr1  37360  cvrval4N  37435  cvrat3  37463  3noncolr2  37470  4noncolr3  37474  3dimlem3  37482  3dimlem3OLDN  37483  3dimlem4  37485  3dimlem4OLDN  37486  llncvrlpln  37579  lplncvrlvol  37637  snatpsubN  37771  linepsubN  37773  pmapjat1  37874  pclfinclN  37971  pl42N  38004  ltrneq2  38169  cdleme7aa  38263  cdleme18d  38316  cdleme21b  38347  trlord  38590  trlcoat  38744  dochkrshp  39407  lcfl8  39523  mulgt0con1dlem  40434  irrapxlem2  40652  pell14qrdich  40698  monotoddzz  40772  pw2f1ocnv  40866  iocinico  41050  harval3  41152  sbcim2g  42165  stoweidlem62  43610  elfzelfzlble  44824  1arymaptf1  45999  2arymaptf1  46010  eenglngeehlnmlem2  46095  mpbiran3d  46153  opnneil  46214