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  3826  opeldmd  5917  elreldm  5946  predtrss  6343  ordtr2  6428  ssimaex  6994  fliftfun  7332  isopolem  7365  isosolem  7367  ordsucss  7838  f1oweALT  7997  fnse  8158  soseq  8184  brtpos  8260  issmo2  8389  seqomlem1  8490  omcl  8574  oecl  8575  oawordeulem  8592  oaass  8599  omordi  8604  omord  8606  odi  8617  oen0  8624  oeordi  8625  oeordsuc  8632  nnmcl  8650  nnecl  8651  nnmordi  8669  nnmord  8670  nnmwordri  8674  nnaordex  8676  swoord1  8777  ecopovtrn  8860  f1domg  9012  pw2f1olem  9116  domtriord  9163  mapen  9181  mapxpen  9183  mapunen  9186  nndomog  9253  nndomogOLD  9263  onomeneq  9265  inficl  9465  supmo  9492  infmo  9535  inf3lem6  9673  cantnflem1  9729  tcmin  9781  tcrank  9924  cardne  10005  cardlim  10012  cardsdomel  10014  carduni  10021  alephord  10115  cardinfima  10137  dfac5lem4  10166  dfac5lem4OLD  10168  infdif2  10249  cofsmo  10309  cfcoflem  10312  infpssrlem4  10346  infpssrlem5  10347  fin4en1  10349  isfin2-2  10359  enfin2i  10361  fin23lem27  10368  isf32lem12  10404  isf34lem6  10420  domtriomlem  10482  cardmin  10604  fpwwe2lem11  10681  inar1  10815  gruiun  10839  ltsonq  11009  prub  11034  reclem3pr  11089  mulcmpblnr  11111  mulgt0sr  11145  axpre-sup  11209  leltadd  11747  infm3  12227  peano5nni  12269  zextle  12691  prime  12699  uzin  12918  ublbneg  12975  zbtwnre  12988  mul2lt0bi  13141  xrre2  13212  xralrple  13247  xmulneg1  13311  supxrbnd  13370  supxrgtmnf  13371  fzrevral  13652  flge  13845  ceile  13889  modadd1  13948  modmul1  13965  modsumfzodifsn  13985  seqcl2  14061  facdiv  14326  hashss  14448  hash2exprb  14510  elfzelfzccat  14618  repswswrd  14822  cshf1  14848  cshwcsh2id  14867  rlim2lt  15533  rlim3  15534  o1lo1  15573  climshftlem  15610  o1co  15622  o1of2  15649  isercolllem2  15702  isercoll  15704  caucvgrlem2  15711  climcndslem2  15886  sqrt2irr  16285  dvds2lem  16306  dvdsle  16347  dvdsfac  16363  ltoddhalfle  16398  divalglem0  16430  ndvdsadd  16447  bitsinv1lem  16478  sadcaddlem  16494  dvdslegcd  16541  bezoutlem2  16577  bezoutlem4  16579  gcdzeq  16589  algcvga  16616  rpdvds  16697  cncongr1  16704  cncongr2  16705  prmind2  16722  isprm6  16751  rpexp  16759  eulerthlem2  16819  pclem  16876  pceulem  16883  pc2dvds  16917  fldivp1  16935  infpnlem1  16948  prmunb  16952  mrieqv2d  17682  plttr  18387  clatl  18553  issubg4  19163  gexdvds  19602  pgpssslw  19632  sylow2alem2  19636  efgs1b  19754  efgsfo  19757  imasabl  19894  lspindpi  21134  psgnodpm  21606  psgndif  21620  obselocv  21748  pf1ind  22359  mdetunilem9  22626  fiinbas  22959  bastg  22973  tgcl  22976  opnssneib  23123  clslp  23156  tgcnp  23261  iscnp4  23271  cncls2  23281  cncls  23282  cnntr  23283  cnpresti  23296  lmss  23306  lmcnp  23312  cmpsub  23408  tgcmp  23409  dfconn2  23427  t1connperf  23444  1stcfb  23453  1stcrest  23461  kgenss  23551  llycmpkgen2  23558  txdis  23640  qtoptop2  23707  kqt0lem  23744  isr0  23745  regr1lem2  23748  cmphaushmeo  23808  fbun  23848  ssfg  23880  fgtr  23898  ufildr  23939  cnpflf  24009  fclsnei  24027  flimfnfcls  24036  fclscmp  24038  ufilcmp  24040  cnpfcf  24049  alexsublem  24052  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem3  24062  tgphaus  24125  tgpt1  24126  tsmsres  24152  imasdsf1olem  24383  xblss2ps  24411  xblss2  24412  blsscls2  24517  metequiv2  24523  stdbdxmet  24528  nmoi  24749  reconn  24850  mulc1cncf  24931  cncfco  24933  iccpnfhmeo  24976  xrhmeo  24977  evth  24991  pi1grplem  25082  fgcfil  25305  ivthlem2  25487  ivthlem3  25488  ovolicc2lem4  25555  voliunlem1  25585  ioombl1lem4  25596  itg2gt0  25795  limcco  25928  lhop1  26053  tdeglem4  26099  plypf1  26251  coeeulem  26263  coeidlem  26276  coeid3  26279  plymul0or  26322  dvnply2  26329  plydivex  26339  vieta1lem2  26353  plyexmo  26355  aaliou3lem2  26385  ulmss  26440  ulmdvlem3  26445  iblulm  26450  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  logcnlem5  26688  dcubic  26889  amgm  27034  isnsqf  27178  mumullem2  27223  chtublem  27255  chtub  27256  fsumvma2  27258  vmasum  27260  dchrfi  27299  bposlem1  27328  bposlem3  27330  bposlem7  27334  lgsdir  27376  lgsquadlem2  27425  2sqlem8a  27469  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  pntlemf  27649  pntlem3  27653  peano5uzs  28390  axeuclid  28978  uspgrushgr  29194  uspgrupgr  29195  usgruspgr  29197  usgr2pth  29784  crctcshwlkn0lem5  29834  wwlksnext  29913  wwlksnextsurj  29920  clwwlkccatlem  30008  clwlkclwwlkf  30027  clwwisshclwwslemlem  30032  lnon0  30817  normpyc  31165  ocsh  31302  ocorth  31310  ococss  31312  shsel2  31341  hsupss  31360  pjhth  31412  shlub  31433  cm2j  31639  lnfncnbd  32076  riesz1  32084  rnbra  32126  leopadd  32151  leopmuli  32152  hstles  32250  stge1i  32257  stle0i  32258  dmdbr5  32327  ssmd2  32331  superpos  32373  chcv1  32374  atoml2i  32402  chirredlem2  32410  atcvat3i  32415  mdsymlem5  32426  mdsymlem6  32427  sumdmdii  32434  sumdmdlem2  32438  isarchiofld  33347  sqsscirc2  33908  cnre2csqlem  33909  xrge0iifiso  33934  sigaclci  34133  omssubadd  34302  eulerpartlemb  34370  ballotlemimin  34508  ballotlem7  34538  fineqvac  35111  subgrwlk  35137  cusgracyclt3v  35161  cvmlift2lem12  35319  fmlasucdisj  35404  dfon2lem8  35791  segconeq  36011  ifscgr  36045  brofs2  36078  brifs2  36079  endofsegid  36086  dissneqlem  37341  rdgellim  37377  fvineqsneq  37413  tan2h  37619  matunitlindflem2  37624  poimirlem31  37658  poimir  37660  fzmul  37748  fdc  37752  incsequz2  37756  sstotbnd2  37781  sstotbnd3  37783  totbndbnd  37796  isexid2  37862  ispridl2  38045  mpobi123f  38169  disjlem18  38801  disjdmqsss  38803  riotasvd  38957  lsator0sp  39002  lssatle  39016  lshpset2N  39120  lkrlspeqN  39172  omllaw2N  39245  cmtbr3N  39255  lecmtN  39257  cvlcvr1  39340  cvrval4N  39416  cvrat3  39444  3noncolr2  39451  4noncolr3  39455  3dimlem3  39463  3dimlem3OLDN  39464  3dimlem4  39466  3dimlem4OLDN  39467  llncvrlpln  39560  lplncvrlvol  39618  snatpsubN  39752  linepsubN  39754  pmapjat1  39855  pclfinclN  39952  pl42N  39985  ltrneq2  40150  cdleme7aa  40244  cdleme18d  40297  cdleme21b  40328  trlord  40571  trlcoat  40725  dochkrshp  41388  lcfl8  41504  mulgt0con1dlem  42487  irrapxlem2  42834  pell14qrdich  42880  monotoddzz  42955  pw2f1ocnv  43049  iocinico  43224  ordnexbtwnsuc  43280  tfsconcat0i  43358  naddwordnexlem4  43414  harval3  43551  sbcim2g  44558  stoweidlem62  46077  elfzelfzlble  47333  1arymaptf1  48563  2arymaptf1  48574  eenglngeehlnmlem2  48659  mpbiran3d  48717  opnneil  48807