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 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  3815  opeldmd  5906  elreldm  5934  predtrss  6323  ordtr2  6408  ssimaex  6976  fliftfun  7312  isopolem  7345  isosolem  7347  ordsucss  7810  f1oweALT  7963  fnse  8124  soseq  8150  brtpos  8226  issmo2  8355  seqomlem1  8456  omcl  8542  oecl  8543  oawordeulem  8560  oaass  8567  omordi  8572  omord  8574  odi  8585  oen0  8592  oeordi  8593  oeordsuc  8600  nnmcl  8618  nnecl  8619  nnmordi  8637  nnmord  8638  nnmwordri  8642  nnaordex  8644  swoord1  8740  ecopovtrn  8820  f1domg  8974  pw2f1olem  9082  domtriord  9129  mapen  9147  mapxpen  9149  mapunen  9152  nndomog  9222  nndomogOLD  9232  onomeneq  9234  inficl  9426  supmo  9453  infmo  9496  inf3lem6  9634  cantnflem1  9690  tcmin  9742  tcrank  9885  cardne  9966  cardlim  9973  cardsdomel  9975  carduni  9982  alephord  10076  cardinfima  10098  dfac5lem4  10127  infdif2  10211  cofsmo  10270  cfcoflem  10273  infpssrlem4  10307  infpssrlem5  10308  fin4en1  10310  isfin2-2  10320  enfin2i  10322  fin23lem27  10329  isf32lem12  10365  isf34lem6  10381  domtriomlem  10443  cardmin  10565  fpwwe2lem11  10642  inar1  10776  gruiun  10800  ltsonq  10970  prub  10995  reclem3pr  11050  mulcmpblnr  11072  mulgt0sr  11106  axpre-sup  11170  leltadd  11705  infm3  12180  peano5nni  12222  zextle  12642  prime  12650  uzin  12869  ublbneg  12924  zbtwnre  12937  mul2lt0bi  13087  xrre2  13156  xralrple  13191  xmulneg1  13255  supxrbnd  13314  supxrgtmnf  13315  fzrevral  13593  flge  13777  ceile  13821  modadd1  13880  modmul1  13896  modsumfzodifsn  13916  seqcl2  13993  facdiv  14254  hashss  14376  hash2exprb  14439  elfzelfzccat  14537  repswswrd  14741  cshf1  14767  cshwcsh2id  14786  rlim2lt  15448  rlim3  15449  o1lo1  15488  climshftlem  15525  o1co  15537  o1of2  15564  isercolllem2  15619  isercoll  15621  caucvgrlem2  15628  climcndslem2  15803  sqrt2irr  16199  dvds2lem  16219  dvdsle  16260  dvdsfac  16276  ltoddhalfle  16311  divalglem0  16343  ndvdsadd  16360  bitsinv1lem  16389  sadcaddlem  16405  dvdslegcd  16452  bezoutlem2  16489  bezoutlem4  16491  gcdzeq  16501  algcvga  16523  rpdvds  16604  cncongr1  16611  cncongr2  16612  prmind2  16629  isprm6  16658  rpexp  16666  eulerthlem2  16722  pclem  16778  pceulem  16785  pc2dvds  16819  fldivp1  16837  infpnlem1  16850  prmunb  16854  mrieqv2d  17590  plttr  18305  clatl  18471  issubg4  19068  gexdvds  19500  pgpssslw  19530  sylow2alem2  19534  efgs1b  19652  efgsfo  19655  imasabl  19792  lspindpi  20979  psgnodpm  21452  psgndif  21466  obselocv  21594  pf1ind  22195  mdetunilem9  22443  fiinbas  22776  bastg  22790  tgcl  22793  opnssneib  22940  clslp  22973  tgcnp  23078  iscnp4  23088  cncls2  23098  cncls  23099  cnntr  23100  cnpresti  23113  lmss  23123  lmcnp  23129  cmpsub  23225  tgcmp  23226  dfconn2  23244  t1connperf  23261  1stcfb  23270  1stcrest  23278  kgenss  23368  llycmpkgen2  23375  txdis  23457  qtoptop2  23524  kqt0lem  23561  isr0  23562  regr1lem2  23565  cmphaushmeo  23625  fbun  23665  ssfg  23697  fgtr  23715  ufildr  23756  cnpflf  23826  fclsnei  23844  flimfnfcls  23853  fclscmp  23855  ufilcmp  23857  cnpfcf  23866  alexsublem  23869  alexsubALTlem3  23874  alexsubALTlem4  23875  ptcmplem3  23879  tgphaus  23942  tgpt1  23943  tsmsres  23969  imasdsf1olem  24200  xblss2ps  24228  xblss2  24229  blsscls2  24334  metequiv2  24340  stdbdxmet  24345  nmoi  24566  reconn  24665  mulc1cncf  24746  cncfco  24748  iccpnfhmeo  24791  xrhmeo  24792  evth  24806  pi1grplem  24897  fgcfil  25120  ivthlem2  25302  ivthlem3  25303  ovolicc2lem4  25370  voliunlem1  25400  ioombl1lem4  25411  itg2gt0  25611  limcco  25743  lhop1  25868  tdeglem4  25916  tdeglem4OLD  25917  plypf1  26065  coeeulem  26077  coeidlem  26090  coeid3  26093  plymul0or  26134  dvnply2  26140  plydivex  26150  vieta1lem2  26164  plyexmo  26166  aaliou3lem2  26196  ulmss  26249  ulmdvlem3  26254  iblulm  26259  sincosq2sgn  26350  sincosq3sgn  26351  sincosq4sgn  26352  logcnlem5  26495  dcubic  26693  amgm  26838  isnsqf  26982  mumullem2  27027  chtublem  27059  chtub  27060  fsumvma2  27062  vmasum  27064  dchrfi  27103  bposlem1  27132  bposlem3  27134  bposlem7  27138  lgsdir  27180  lgsquadlem2  27229  2sqlem8a  27273  2sqlem10  27276  dchrisum0flb  27358  pntpbnd1  27434  pntlemf  27453  pntlem3  27457  axeuclid  28656  uspgrushgr  28870  uspgrupgr  28871  usgruspgr  28873  usgr2pth  29456  crctcshwlkn0lem5  29503  wwlksnext  29582  wwlksnextsurj  29589  clwwlkccatlem  29677  clwlkclwwlkf  29696  clwwisshclwwslemlem  29701  lnon0  30486  normpyc  30834  ocsh  30971  ocorth  30979  ococss  30981  shsel2  31010  hsupss  31029  pjhth  31081  shlub  31102  cm2j  31308  lnfncnbd  31745  riesz1  31753  rnbra  31795  leopadd  31820  leopmuli  31821  hstles  31919  stge1i  31926  stle0i  31927  dmdbr5  31996  ssmd2  32000  superpos  32042  chcv1  32043  atoml2i  32071  chirredlem2  32079  atcvat3i  32084  mdsymlem5  32095  mdsymlem6  32096  sumdmdii  32103  sumdmdlem2  32107  isarchiofld  32873  sqsscirc2  33355  cnre2csqlem  33356  xrge0iifiso  33381  sigaclci  33596  omssubadd  33765  eulerpartlemb  33833  ballotlemimin  33970  ballotlem7  34000  fineqvac  34563  subgrwlk  34589  cusgracyclt3v  34613  cvmlift2lem12  34771  fmlasucdisj  34856  dfon2lem8  35234  segconeq  35454  ifscgr  35488  brofs2  35521  brifs2  35522  endofsegid  35529  dissneqlem  36688  rdgellim  36724  fvineqsneq  36760  tan2h  36947  matunitlindflem2  36952  poimirlem31  36986  poimir  36988  fzmul  37076  fdc  37080  incsequz2  37084  sstotbnd2  37109  sstotbnd3  37111  totbndbnd  37124  isexid2  37190  ispridl2  37373  mpobi123f  37497  disjlem18  38137  disjdmqsss  38139  riotasvd  38293  lsator0sp  38338  lssatle  38352  lshpset2N  38456  lkrlspeqN  38508  omllaw2N  38581  cmtbr3N  38591  lecmtN  38593  cvlcvr1  38676  cvrval4N  38752  cvrat3  38780  3noncolr2  38787  4noncolr3  38791  3dimlem3  38799  3dimlem3OLDN  38800  3dimlem4  38802  3dimlem4OLDN  38803  llncvrlpln  38896  lplncvrlvol  38954  snatpsubN  39088  linepsubN  39090  pmapjat1  39191  pclfinclN  39288  pl42N  39321  ltrneq2  39486  cdleme7aa  39580  cdleme18d  39633  cdleme21b  39664  trlord  39907  trlcoat  40061  dochkrshp  40724  lcfl8  40840  mulgt0con1dlem  41796  irrapxlem2  42027  pell14qrdich  42073  monotoddzz  42148  pw2f1ocnv  42242  iocinico  42427  ordnexbtwnsuc  42483  tfsconcat0i  42561  naddwordnexlem4  42618  harval3  42755  sbcim2g  43765  stoweidlem62  45240  elfzelfzlble  46491  1arymaptf1  47493  2arymaptf1  47504  eenglngeehlnmlem2  47589  mpbiran3d  47647  opnneil  47707