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  3782  opeldmd  5853  elreldm  5881  predtrss  6274  ordtr2  6356  ssimaex  6912  fliftfun  7253  isopolem  7286  isosolem  7288  ordsucss  7757  f1oweALT  7914  fnse  8073  soseq  8099  brtpos  8175  issmo2  8279  seqomlem1  8379  omcl  8461  oecl  8462  oawordeulem  8479  oaass  8486  omordi  8491  omord  8493  odi  8504  oen0  8511  oeordi  8512  oeordsuc  8519  nnmcl  8537  nnecl  8538  nnmordi  8556  nnmord  8557  nnmwordri  8561  nnaordex  8563  swoord1  8664  ecopovtrn  8754  f1domg  8904  pw2f1olem  9005  domtriord  9047  mapen  9065  mapxpen  9067  mapunen  9070  nndomog  9137  onomeneq  9138  inficl  9334  supmo  9361  infmo  9406  inf3lem6  9548  cantnflem1  9604  tcmin  9656  tcrank  9799  cardne  9880  cardlim  9887  cardsdomel  9889  carduni  9896  alephord  9988  cardinfima  10010  dfac5lem4  10039  dfac5lem4OLD  10041  infdif2  10122  cofsmo  10182  cfcoflem  10185  infpssrlem4  10219  infpssrlem5  10220  fin4en1  10222  isfin2-2  10232  enfin2i  10234  fin23lem27  10241  isf32lem12  10277  isf34lem6  10293  domtriomlem  10355  cardmin  10477  fpwwe2lem11  10554  inar1  10688  gruiun  10712  ltsonq  10882  prub  10907  reclem3pr  10962  mulcmpblnr  10984  mulgt0sr  11018  axpre-sup  11082  leltadd  11622  infm3  12102  peano5nni  12149  zextle  12567  prime  12575  uzin  12793  ublbneg  12852  zbtwnre  12865  mul2lt0bi  13019  xrre2  13090  xralrple  13125  xmulneg1  13189  supxrbnd  13248  supxrgtmnf  13249  fzrevral  13533  flge  13727  ceile  13771  modadd1  13830  modmul1  13849  modsumfzodifsn  13869  seqcl2  13945  facdiv  14212  hashss  14334  hash2exprb  14396  elfzelfzccat  14505  repswswrd  14708  cshf1  14734  cshwcsh2id  14753  rlim2lt  15422  rlim3  15423  o1lo1  15462  climshftlem  15499  o1co  15511  o1of2  15538  isercolllem2  15591  isercoll  15593  caucvgrlem2  15600  climcndslem2  15775  sqrt2irr  16176  dvds2lem  16197  dvdsle  16239  dvdsfac  16255  ltoddhalfle  16290  divalglem0  16322  ndvdsadd  16339  bitsinv1lem  16370  sadcaddlem  16386  dvdslegcd  16433  bezoutlem2  16469  bezoutlem4  16471  gcdzeq  16481  algcvga  16508  rpdvds  16589  cncongr1  16596  cncongr2  16597  prmind2  16614  isprm6  16643  rpexp  16651  eulerthlem2  16711  pclem  16768  pceulem  16775  pc2dvds  16809  fldivp1  16827  infpnlem1  16840  prmunb  16844  mrieqv2d  17563  plttr  18264  clatl  18432  issubg4  19042  gexdvds  19481  pgpssslw  19511  sylow2alem2  19515  efgs1b  19633  efgsfo  19636  imasabl  19773  lspindpi  21057  psgnodpm  21513  psgndif  21527  obselocv  21653  pf1ind  22258  mdetunilem9  22523  fiinbas  22855  bastg  22869  tgcl  22872  opnssneib  23018  clslp  23051  tgcnp  23156  iscnp4  23166  cncls2  23176  cncls  23177  cnntr  23178  cnpresti  23191  lmss  23201  lmcnp  23207  cmpsub  23303  tgcmp  23304  dfconn2  23322  t1connperf  23339  1stcfb  23348  1stcrest  23356  kgenss  23446  llycmpkgen2  23453  txdis  23535  qtoptop2  23602  kqt0lem  23639  isr0  23640  regr1lem2  23643  cmphaushmeo  23703  fbun  23743  ssfg  23775  fgtr  23793  ufildr  23834  cnpflf  23904  fclsnei  23922  flimfnfcls  23931  fclscmp  23933  ufilcmp  23935  cnpfcf  23944  alexsublem  23947  alexsubALTlem3  23952  alexsubALTlem4  23953  ptcmplem3  23957  tgphaus  24020  tgpt1  24021  tsmsres  24047  imasdsf1olem  24277  xblss2ps  24305  xblss2  24306  blsscls2  24408  metequiv2  24414  stdbdxmet  24419  nmoi  24632  reconn  24733  mulc1cncf  24814  cncfco  24816  iccpnfhmeo  24859  xrhmeo  24860  evth  24874  pi1grplem  24965  fgcfil  25187  ivthlem2  25369  ivthlem3  25370  ovolicc2lem4  25437  voliunlem1  25467  ioombl1lem4  25478  itg2gt0  25677  limcco  25810  lhop1  25935  tdeglem4  25981  plypf1  26133  coeeulem  26145  coeidlem  26158  coeid3  26161  plymul0or  26204  dvnply2  26211  plydivex  26221  vieta1lem2  26235  plyexmo  26237  aaliou3lem2  26267  ulmss  26322  ulmdvlem3  26327  iblulm  26332  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  logcnlem5  26571  dcubic  26772  amgm  26917  isnsqf  27061  mumullem2  27106  chtublem  27138  chtub  27139  fsumvma2  27141  vmasum  27143  dchrfi  27182  bposlem1  27211  bposlem3  27213  bposlem7  27217  lgsdir  27259  lgsquadlem2  27308  2sqlem8a  27352  2sqlem10  27355  dchrisum0flb  27437  pntpbnd1  27513  pntlemf  27532  pntlem3  27536  peano5uzs  28315  axeuclid  28926  uspgrushgr  29140  uspgrupgr  29141  usgruspgr  29143  usgr2pth  29727  crctcshwlkn0lem5  29777  wwlksnext  29856  wwlksnextsurj  29863  clwwlkccatlem  29951  clwlkclwwlkf  29970  clwwisshclwwslemlem  29975  lnon0  30760  normpyc  31108  ocsh  31245  ocorth  31253  ococss  31255  shsel2  31284  hsupss  31303  pjhth  31355  shlub  31376  cm2j  31582  lnfncnbd  32019  riesz1  32027  rnbra  32069  leopadd  32094  leopmuli  32095  hstles  32193  stge1i  32200  stle0i  32201  dmdbr5  32270  ssmd2  32274  superpos  32316  chcv1  32317  atoml2i  32345  chirredlem2  32353  atcvat3i  32358  mdsymlem5  32369  mdsymlem6  32370  sumdmdii  32377  sumdmdlem2  32381  isarchiofld  33151  sqsscirc2  33875  cnre2csqlem  33876  xrge0iifiso  33901  sigaclci  34098  omssubadd  34267  eulerpartlemb  34335  ballotlemimin  34473  ballotlem7  34503  fineqvac  35071  vonf1owev  35080  subgrwlk  35104  cusgracyclt3v  35128  cvmlift2lem12  35286  fmlasucdisj  35371  dfon2lem8  35763  segconeq  35983  ifscgr  36017  brofs2  36050  brifs2  36051  endofsegid  36058  dissneqlem  37313  rdgellim  37349  fvineqsneq  37385  tan2h  37591  matunitlindflem2  37596  poimirlem31  37630  poimir  37632  fzmul  37720  fdc  37724  incsequz2  37728  sstotbnd2  37753  sstotbnd3  37755  totbndbnd  37768  isexid2  37834  ispridl2  38017  mpobi123f  38141  disjlem18  38777  disjdmqsss  38779  riotasvd  38934  lsator0sp  38979  lssatle  38993  lshpset2N  39097  lkrlspeqN  39149  omllaw2N  39222  cmtbr3N  39232  lecmtN  39234  cvlcvr1  39317  cvrval4N  39393  cvrat3  39421  3noncolr2  39428  4noncolr3  39432  3dimlem3  39440  3dimlem3OLDN  39441  3dimlem4  39443  3dimlem4OLDN  39444  llncvrlpln  39537  lplncvrlvol  39595  snatpsubN  39729  linepsubN  39731  pmapjat1  39832  pclfinclN  39929  pl42N  39962  ltrneq2  40127  cdleme7aa  40221  cdleme18d  40274  cdleme21b  40305  trlord  40548  trlcoat  40702  dochkrshp  41365  lcfl8  41481  mulgt0con1dlem  42442  irrapxlem2  42796  pell14qrdich  42842  monotoddzz  42916  pw2f1ocnv  43010  iocinico  43185  ordnexbtwnsuc  43240  tfsconcat0i  43318  naddwordnexlem4  43374  harval3  43511  sbcim2g  44512  stoweidlem62  46044  elfzelfzlble  47306  pgnbgreunbgrlem1  48087  pgnbgreunbgrlem4  48093  1arymaptf1  48615  2arymaptf1  48626  eenglngeehlnmlem2  48711  mpbiran3d  48769  opnneil  48882