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  3843  opeldmd  5931  elreldm  5960  predtrss  6354  ordtr2  6439  ssimaex  7007  fliftfun  7348  isopolem  7381  isosolem  7383  ordsucss  7854  f1oweALT  8013  fnse  8174  soseq  8200  brtpos  8276  issmo2  8405  seqomlem1  8506  omcl  8592  oecl  8593  oawordeulem  8610  oaass  8617  omordi  8622  omord  8624  odi  8635  oen0  8642  oeordi  8643  oeordsuc  8650  nnmcl  8668  nnecl  8669  nnmordi  8687  nnmord  8688  nnmwordri  8692  nnaordex  8694  swoord1  8795  ecopovtrn  8878  f1domg  9032  pw2f1olem  9142  domtriord  9189  mapen  9207  mapxpen  9209  mapunen  9212  nndomog  9279  nndomogOLD  9289  onomeneq  9291  inficl  9494  supmo  9521  infmo  9564  inf3lem6  9702  cantnflem1  9758  tcmin  9810  tcrank  9953  cardne  10034  cardlim  10041  cardsdomel  10043  carduni  10050  alephord  10144  cardinfima  10166  dfac5lem4  10195  dfac5lem4OLD  10197  infdif2  10278  cofsmo  10338  cfcoflem  10341  infpssrlem4  10375  infpssrlem5  10376  fin4en1  10378  isfin2-2  10388  enfin2i  10390  fin23lem27  10397  isf32lem12  10433  isf34lem6  10449  domtriomlem  10511  cardmin  10633  fpwwe2lem11  10710  inar1  10844  gruiun  10868  ltsonq  11038  prub  11063  reclem3pr  11118  mulcmpblnr  11140  mulgt0sr  11174  axpre-sup  11238  leltadd  11774  infm3  12254  peano5nni  12296  zextle  12716  prime  12724  uzin  12943  ublbneg  12998  zbtwnre  13011  mul2lt0bi  13163  xrre2  13232  xralrple  13267  xmulneg1  13331  supxrbnd  13390  supxrgtmnf  13391  fzrevral  13669  flge  13856  ceile  13900  modadd1  13959  modmul1  13975  modsumfzodifsn  13995  seqcl2  14071  facdiv  14336  hashss  14458  hash2exprb  14520  elfzelfzccat  14628  repswswrd  14832  cshf1  14858  cshwcsh2id  14877  rlim2lt  15543  rlim3  15544  o1lo1  15583  climshftlem  15620  o1co  15632  o1of2  15659  isercolllem2  15714  isercoll  15716  caucvgrlem2  15723  climcndslem2  15898  sqrt2irr  16297  dvds2lem  16317  dvdsle  16358  dvdsfac  16374  ltoddhalfle  16409  divalglem0  16441  ndvdsadd  16458  bitsinv1lem  16487  sadcaddlem  16503  dvdslegcd  16550  bezoutlem2  16587  bezoutlem4  16589  gcdzeq  16599  algcvga  16626  rpdvds  16707  cncongr1  16714  cncongr2  16715  prmind2  16732  isprm6  16761  rpexp  16769  eulerthlem2  16829  pclem  16885  pceulem  16892  pc2dvds  16926  fldivp1  16944  infpnlem1  16957  prmunb  16961  mrieqv2d  17697  plttr  18412  clatl  18578  issubg4  19185  gexdvds  19626  pgpssslw  19656  sylow2alem2  19660  efgs1b  19778  efgsfo  19781  imasabl  19918  lspindpi  21157  psgnodpm  21629  psgndif  21643  obselocv  21771  pf1ind  22380  mdetunilem9  22647  fiinbas  22980  bastg  22994  tgcl  22997  opnssneib  23144  clslp  23177  tgcnp  23282  iscnp4  23292  cncls2  23302  cncls  23303  cnntr  23304  cnpresti  23317  lmss  23327  lmcnp  23333  cmpsub  23429  tgcmp  23430  dfconn2  23448  t1connperf  23465  1stcfb  23474  1stcrest  23482  kgenss  23572  llycmpkgen2  23579  txdis  23661  qtoptop2  23728  kqt0lem  23765  isr0  23766  regr1lem2  23769  cmphaushmeo  23829  fbun  23869  ssfg  23901  fgtr  23919  ufildr  23960  cnpflf  24030  fclsnei  24048  flimfnfcls  24057  fclscmp  24059  ufilcmp  24061  cnpfcf  24070  alexsublem  24073  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem3  24083  tgphaus  24146  tgpt1  24147  tsmsres  24173  imasdsf1olem  24404  xblss2ps  24432  xblss2  24433  blsscls2  24538  metequiv2  24544  stdbdxmet  24549  nmoi  24770  reconn  24869  mulc1cncf  24950  cncfco  24952  iccpnfhmeo  24995  xrhmeo  24996  evth  25010  pi1grplem  25101  fgcfil  25324  ivthlem2  25506  ivthlem3  25507  ovolicc2lem4  25574  voliunlem1  25604  ioombl1lem4  25615  itg2gt0  25815  limcco  25948  lhop1  26073  tdeglem4  26119  plypf1  26271  coeeulem  26283  coeidlem  26296  coeid3  26299  plymul0or  26340  dvnply2  26347  plydivex  26357  vieta1lem2  26371  plyexmo  26373  aaliou3lem2  26403  ulmss  26458  ulmdvlem3  26463  iblulm  26468  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  logcnlem5  26706  dcubic  26907  amgm  27052  isnsqf  27196  mumullem2  27241  chtublem  27273  chtub  27274  fsumvma2  27276  vmasum  27278  dchrfi  27317  bposlem1  27346  bposlem3  27348  bposlem7  27352  lgsdir  27394  lgsquadlem2  27443  2sqlem8a  27487  2sqlem10  27490  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  pntlem3  27671  peano5uzs  28408  axeuclid  28996  uspgrushgr  29212  uspgrupgr  29213  usgruspgr  29215  usgr2pth  29800  crctcshwlkn0lem5  29847  wwlksnext  29926  wwlksnextsurj  29933  clwwlkccatlem  30021  clwlkclwwlkf  30040  clwwisshclwwslemlem  30045  lnon0  30830  normpyc  31178  ocsh  31315  ocorth  31323  ococss  31325  shsel2  31354  hsupss  31373  pjhth  31425  shlub  31446  cm2j  31652  lnfncnbd  32089  riesz1  32097  rnbra  32139  leopadd  32164  leopmuli  32165  hstles  32263  stge1i  32270  stle0i  32271  dmdbr5  32340  ssmd2  32344  superpos  32386  chcv1  32387  atoml2i  32415  chirredlem2  32423  atcvat3i  32428  mdsymlem5  32439  mdsymlem6  32440  sumdmdii  32447  sumdmdlem2  32451  isarchiofld  33312  sqsscirc2  33855  cnre2csqlem  33856  xrge0iifiso  33881  sigaclci  34096  omssubadd  34265  eulerpartlemb  34333  ballotlemimin  34470  ballotlem7  34500  fineqvac  35073  subgrwlk  35100  cusgracyclt3v  35124  cvmlift2lem12  35282  fmlasucdisj  35367  dfon2lem8  35754  segconeq  35974  ifscgr  36008  brofs2  36041  brifs2  36042  endofsegid  36049  dissneqlem  37306  rdgellim  37342  fvineqsneq  37378  tan2h  37572  matunitlindflem2  37577  poimirlem31  37611  poimir  37613  fzmul  37701  fdc  37705  incsequz2  37709  sstotbnd2  37734  sstotbnd3  37736  totbndbnd  37749  isexid2  37815  ispridl2  37998  mpobi123f  38122  disjlem18  38756  disjdmqsss  38758  riotasvd  38912  lsator0sp  38957  lssatle  38971  lshpset2N  39075  lkrlspeqN  39127  omllaw2N  39200  cmtbr3N  39210  lecmtN  39212  cvlcvr1  39295  cvrval4N  39371  cvrat3  39399  3noncolr2  39406  4noncolr3  39410  3dimlem3  39418  3dimlem3OLDN  39419  3dimlem4  39421  3dimlem4OLDN  39422  llncvrlpln  39515  lplncvrlvol  39573  snatpsubN  39707  linepsubN  39709  pmapjat1  39810  pclfinclN  39907  pl42N  39940  ltrneq2  40105  cdleme7aa  40199  cdleme18d  40252  cdleme21b  40283  trlord  40526  trlcoat  40680  dochkrshp  41343  lcfl8  41459  mulgt0con1dlem  42433  irrapxlem2  42779  pell14qrdich  42825  monotoddzz  42900  pw2f1ocnv  42994  iocinico  43173  ordnexbtwnsuc  43229  tfsconcat0i  43307  naddwordnexlem4  43363  harval3  43500  sbcim2g  44509  stoweidlem62  45983  elfzelfzlble  47236  1arymaptf1  48376  2arymaptf1  48387  eenglngeehlnmlem2  48472  mpbiran3d  48530  opnneil  48589