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  3779  opeldmd  5856  elreldm  5885  predtrss  6281  ordtr2  6363  ssimaex  6920  fliftfun  7260  isopolem  7293  isosolem  7295  ordsucss  7762  f1oweALT  7918  fnse  8077  soseq  8103  brtpos  8179  issmo2  8283  seqomlem1  8383  omcl  8465  oecl  8466  oawordeulem  8483  oaass  8490  omordi  8495  omord  8497  odi  8508  oen0  8516  oeordi  8517  oeordsuc  8524  nnmcl  8542  nnecl  8543  nnmordi  8561  nnmord  8562  nnmwordri  8566  nnaordex  8568  swoord1  8670  ecopovtrn  8761  f1domg  8912  pw2f1olem  9013  domtriord  9055  mapen  9073  mapxpen  9075  mapunen  9078  nndomog  9141  onomeneq  9142  inficl  9332  supmo  9359  infmo  9404  inf3lem6  9546  cantnflem1  9602  tcmin  9652  tcrank  9800  cardne  9881  cardlim  9888  cardsdomel  9890  carduni  9897  alephord  9989  cardinfima  10011  dfac5lem4  10040  dfac5lem4OLD  10042  infdif2  10123  cofsmo  10183  cfcoflem  10186  infpssrlem4  10220  infpssrlem5  10221  fin4en1  10223  isfin2-2  10233  enfin2i  10235  fin23lem27  10242  isf32lem12  10278  isf34lem6  10294  domtriomlem  10356  cardmin  10478  fpwwe2lem11  10556  inar1  10690  gruiun  10714  ltsonq  10884  prub  10909  reclem3pr  10964  mulcmpblnr  10986  mulgt0sr  11020  axpre-sup  11084  leltadd  11625  infm3  12105  peano5nni  12152  zextle  12569  prime  12577  uzin  12791  ublbneg  12850  zbtwnre  12863  mul2lt0bi  13017  xrre2  13089  xralrple  13124  xmulneg1  13188  supxrbnd  13247  supxrgtmnf  13248  fzrevral  13532  flge  13729  ceile  13773  modadd1  13832  modmul1  13851  modsumfzodifsn  13871  seqcl2  13947  facdiv  14214  hashss  14336  hash2exprb  14398  elfzelfzccat  14507  repswswrd  14711  cshf1  14737  cshwcsh2id  14755  rlim2lt  15424  rlim3  15425  o1lo1  15464  climshftlem  15501  o1co  15513  o1of2  15540  isercolllem2  15593  isercoll  15595  caucvgrlem2  15602  climcndslem2  15777  sqrt2irr  16178  dvds2lem  16199  dvdsle  16241  dvdsfac  16257  ltoddhalfle  16292  divalglem0  16324  ndvdsadd  16341  bitsinv1lem  16372  sadcaddlem  16388  dvdslegcd  16435  bezoutlem2  16471  bezoutlem4  16473  gcdzeq  16483  algcvga  16510  rpdvds  16591  cncongr1  16598  cncongr2  16599  prmind2  16616  isprm6  16645  rpexp  16653  eulerthlem2  16713  pclem  16770  pceulem  16777  pc2dvds  16811  fldivp1  16829  infpnlem1  16842  prmunb  16846  mrieqv2d  17566  plttr  18267  clatl  18435  issubg4  19079  gexdvds  19517  pgpssslw  19547  sylow2alem2  19551  efgs1b  19669  efgsfo  19672  imasabl  19809  lspindpi  21091  psgnodpm  21547  psgndif  21561  obselocv  21687  pf1ind  22303  mdetunilem9  22568  fiinbas  22900  bastg  22914  tgcl  22917  opnssneib  23063  clslp  23096  tgcnp  23201  iscnp4  23211  cncls2  23221  cncls  23222  cnntr  23223  cnpresti  23236  lmss  23246  lmcnp  23252  cmpsub  23348  tgcmp  23349  dfconn2  23367  t1connperf  23384  1stcfb  23393  1stcrest  23401  kgenss  23491  llycmpkgen2  23498  txdis  23580  qtoptop2  23647  kqt0lem  23684  isr0  23685  regr1lem2  23688  cmphaushmeo  23748  fbun  23788  ssfg  23820  fgtr  23838  ufildr  23879  cnpflf  23949  fclsnei  23967  flimfnfcls  23976  fclscmp  23978  ufilcmp  23980  cnpfcf  23989  alexsublem  23992  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem3  24002  tgphaus  24065  tgpt1  24066  tsmsres  24092  imasdsf1olem  24321  xblss2ps  24349  xblss2  24350  blsscls2  24452  metequiv2  24458  stdbdxmet  24463  nmoi  24676  reconn  24777  mulc1cncf  24858  cncfco  24860  iccpnfhmeo  24903  xrhmeo  24904  evth  24918  pi1grplem  25009  fgcfil  25231  ivthlem2  25413  ivthlem3  25414  ovolicc2lem4  25481  voliunlem1  25511  ioombl1lem4  25522  itg2gt0  25721  limcco  25854  lhop1  25979  tdeglem4  26025  plypf1  26177  coeeulem  26189  coeidlem  26202  coeid3  26205  plymul0or  26248  dvnply2  26255  plydivex  26265  vieta1lem2  26279  plyexmo  26281  aaliou3lem2  26311  ulmss  26366  ulmdvlem3  26371  iblulm  26376  sincosq2sgn  26468  sincosq3sgn  26469  sincosq4sgn  26470  logcnlem5  26615  dcubic  26816  amgm  26961  isnsqf  27105  mumullem2  27150  chtublem  27182  chtub  27183  fsumvma2  27185  vmasum  27187  dchrfi  27226  bposlem1  27255  bposlem3  27257  bposlem7  27261  lgsdir  27303  lgsquadlem2  27352  2sqlem8a  27396  2sqlem10  27399  dchrisum0flb  27481  pntpbnd1  27557  pntlemf  27576  pntlem3  27580  addsonbday  28260  peano5uzs  28383  axeuclid  29019  uspgrushgr  29233  uspgrupgr  29234  usgruspgr  29236  usgr2pth  29820  crctcshwlkn0lem5  29870  wwlksnext  29949  wwlksnextsurj  29956  clwwlkccatlem  30047  clwlkclwwlkf  30066  clwwisshclwwslemlem  30071  lnon0  30856  normpyc  31204  ocsh  31341  ocorth  31349  ococss  31351  shsel2  31380  hsupss  31399  pjhth  31451  shlub  31472  cm2j  31678  lnfncnbd  32115  riesz1  32123  rnbra  32165  leopadd  32190  leopmuli  32191  hstles  32289  stge1i  32296  stle0i  32297  dmdbr5  32366  ssmd2  32370  superpos  32412  chcv1  32413  atoml2i  32441  chirredlem2  32449  atcvat3i  32454  mdsymlem5  32465  mdsymlem6  32466  sumdmdii  32473  sumdmdlem2  32477  isarchiofld  33262  sqsscirc2  34047  cnre2csqlem  34048  xrge0iifiso  34073  sigaclci  34270  omssubadd  34438  eulerpartlemb  34506  ballotlemimin  34644  ballotlem7  34674  fineqvac  35253  fineqvinfep  35262  vonf1owev  35283  subgrwlk  35307  cusgracyclt3v  35331  cvmlift2lem12  35489  fmlasucdisj  35574  dfon2lem8  35963  segconeq  36185  ifscgr  36219  brofs2  36252  brifs2  36253  endofsegid  36260  dissneqlem  37516  rdgellim  37552  fvineqsneq  37588  tan2h  37784  matunitlindflem2  37789  poimirlem31  37823  poimir  37825  fzmul  37913  fdc  37917  incsequz2  37921  sstotbnd2  37946  sstotbnd3  37948  totbndbnd  37961  isexid2  38027  ispridl2  38210  mpobi123f  38334  disjlem18  39075  disjdmqsss  39077  eldisjs6  39112  riotasvd  39253  lsator0sp  39298  lssatle  39312  lshpset2N  39416  lkrlspeqN  39468  omllaw2N  39541  cmtbr3N  39551  lecmtN  39553  cvlcvr1  39636  cvrval4N  39711  cvrat3  39739  3noncolr2  39746  4noncolr3  39750  3dimlem3  39758  3dimlem3OLDN  39759  3dimlem4  39761  3dimlem4OLDN  39762  llncvrlpln  39855  lplncvrlvol  39913  snatpsubN  40047  linepsubN  40049  pmapjat1  40150  pclfinclN  40247  pl42N  40280  ltrneq2  40445  cdleme7aa  40539  cdleme18d  40592  cdleme21b  40623  trlord  40866  trlcoat  41020  dochkrshp  41683  lcfl8  41799  mulgt0con1dlem  42760  irrapxlem2  43101  pell14qrdich  43147  monotoddzz  43221  pw2f1ocnv  43315  iocinico  43490  ordnexbtwnsuc  43545  tfsconcat0i  43623  naddwordnexlem4  43679  harval3  43815  sbcim2g  44815  stoweidlem62  46342  elfzelfzlble  47603  pgnbgreunbgrlem1  48395  pgnbgreunbgrlem4  48401  1arymaptf1  48924  2arymaptf1  48935  eenglngeehlnmlem2  49020  mpbiran3d  49078  opnneil  49191