Theorem sylibrd 260

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 249	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr4d  295  sbciegft  3742  opeldmd  5668  elreldm  5694  ordtr2  6117  ssimaex  6622  fliftfun  6935  isopolem  6968  isosolem  6970  ordsucss  7396  f1oweALT  7536  fnse  7687  brtpos  7759  issmo2  7845  seqomlem1  7944  omcl  8019  oecl  8020  oawordeulem  8037  oaass  8044  omordi  8049  omord  8051  odi  8062  oen0  8069  oeordi  8070  oeordsuc  8077  nnmcl  8095  nnecl  8096  nnmordi  8114  nnmord  8115  nnmwordri  8119  nnaordex  8121  swoord1  8177  ecopovtrn  8257  f1domg  8384  pw2f1olem  8475  domtriord  8517  mapen  8535  mapxpen  8537  mapunen  8540  nndomo  8565  inficl  8742  supmo  8769  infmo  8812  inf3lem6  8949  cantnflem1  9005  tcmin  9036  tcrank  9166  cardne  9247  cardlim  9254  cardsdomel  9256  carduni  9263  alephord  9354  cardinfima  9376  dfac5lem4  9405  infdif2  9485  cofsmo  9544  cfcoflem  9547  infpssrlem4  9581  infpssrlem5  9582  fin4en1  9584  isfin2-2  9594  enfin2i  9596  fin23lem27  9603  isf32lem12  9639  isf34lem6  9655  domtriomlem  9717  cardmin  9839  fpwwe2lem12  9916  inar1  10050  gruiun  10074  ltsonq  10244  prub  10269  reclem3pr  10324  mulcmpblnr  10346  mulgt0sr  10380  axpre-sup  10444  leltadd  10978  infm3  11454  peano5nni  11495  zextle  11909  prime  11917  uzin  12131  ublbneg  12186  zbtwnre  12199  mul2lt0bi  12349  xrre2  12417  xralrple  12452  xmulneg1  12516  supxrbnd  12575  supxrgtmnf  12576  fzrevral  12846  flge  13029  ceile  13071  modadd1  13130  modmul1  13146  modsumfzodifsn  13166  seqcl2  13242  facdiv  13501  hashss  13622  hash2exprb  13679  elfzelfzccat  13782  repswswrd  13986  cshf1  14012  cshwcsh2id  14030  rlim2lt  14692  rlim3  14693  o1lo1  14732  climshftlem  14769  o1co  14781  o1of2  14807  isercolllem2  14860  isercoll  14862  caucvgrlem2  14869  climcndslem2  15042  sqrt2irr  15439  dvds2lem  15459  dvdsle  15497  dvdsfac  15513  ltoddhalfle  15547  divalglem0  15581  ndvdsadd  15598  bitsinv1lem  15627  sadcaddlem  15643  dvdslegcd  15690  bezoutlem2  15721  bezoutlem4  15723  gcdzeq  15735  algcvga  15756  rpdvds  15837  cncongr1  15844  cncongr2  15845  prmind2  15862  isprm6  15891  rpexp  15897  eulerthlem2  15952  pclem  16008  pceulem  16015  pc2dvds  16048  fldivp1  16066  infpnlem1  16079  prmunb  16083  mrieqv2d  16743  plttr  17413  clatl  17559  issubg4  18056  gexdvds  18443  pgpssslw  18473  sylow2alem2  18477  efgs1b  18593  efgsfo  18596  lspindpi  19598  pf1ind  20204  psgnodpm  20418  psgndif  20432  obselocv  20558  mdetunilem9  20917  fiinbas  21248  bastg  21262  tgcl  21265  opnssneib  21411  clslp  21444  tgcnp  21549  iscnp4  21559  cncls2  21569  cncls  21570  cnntr  21571  cnpresti  21584  lmss  21594  lmcnp  21600  cmpsub  21696  tgcmp  21697  dfconn2  21715  t1connperf  21732  1stcfb  21741  1stcrest  21749  kgenss  21839  llycmpkgen2  21846  txdis  21928  qtoptop2  21995  kqt0lem  22032  isr0  22033  regr1lem2  22036  cmphaushmeo  22096  fbun  22136  ssfg  22168  fgtr  22186  ufildr  22227  cnpflf  22297  fclsnei  22315  flimfnfcls  22324  fclscmp  22326  ufilcmp  22328  cnpfcf  22337  alexsublem  22340  alexsubALTlem3  22345  alexsubALTlem4  22346  ptcmplem3  22350  tgphaus  22412  tgpt1  22413  tsmsres  22439  imasdsf1olem  22670  xblss2ps  22698  xblss2  22699  blsscls2  22801  metequiv2  22807  stdbdxmet  22812  nmoi  23024  reconn  23123  mulc1cncf  23200  cncfco  23202  iccpnfhmeo  23236  xrhmeo  23237  evth  23250  pi1grplem  23340  fgcfil  23561  ivthlem2  23740  ivthlem3  23741  ovolicc2lem4  23808  voliunlem1  23838  ioombl1lem4  23849  itg2gt0  24048  limcco  24178  lhop1  24298  tdeglem4  24341  plypf1  24489  coeeulem  24501  coeidlem  24514  coeid3  24517  plymul0or  24557  dvnply2  24563  plydivex  24573  vieta1lem2  24587  plyexmo  24589  aaliou3lem2  24619  ulmss  24672  ulmdvlem3  24677  iblulm  24682  sincosq2sgn  24772  sincosq3sgn  24773  sincosq4sgn  24774  logcnlem5  24914  dcubic  25109  amgm  25254  isnsqf  25398  mumullem2  25443  chtublem  25473  chtub  25474  fsumvma2  25476  vmasum  25478  dchrfi  25517  bposlem1  25546  bposlem3  25548  bposlem7  25552  lgsdir  25594  lgsquadlem2  25643  2sqlem8a  25687  2sqlem10  25690  dchrisum0flb  25772  pntpbnd1  25848  pntlemf  25867  pntlem3  25871  axeuclid  26436  uspgrushgr  26647  uspgrupgr  26648  usgruspgr  26650  usgr2pth  27231  crctcshwlkn0lem5  27278  wwlksnext  27357  wwlksnextsurj  27364  clwwlkccatlem  27453  clwlkclwwlkf  27472  clwwisshclwwslemlem  27477  lnon0  28262  normpyc  28610  ocsh  28747  ocorth  28755  ococss  28757  shsel2  28786  hsupss  28805  pjhth  28857  shlub  28878  cm2j  29084  lnfncnbd  29521  riesz1  29529  rnbra  29571  leopadd  29596  leopmuli  29597  hstles  29695  stge1i  29702  stle0i  29703  dmdbr5  29772  ssmd2  29776  superpos  29818  chcv1  29819  atoml2i  29847  chirredlem2  29855  atcvat3i  29860  mdsymlem5  29871  mdsymlem6  29872  sumdmdii  29879  sumdmdlem2  29883  isarchiofld  30540  sqsscirc2  30765  cnre2csqlem  30766  xrge0iifiso  30791  sigaclci  31004  omssubadd  31171  eulerpartlemb  31239  ballotlemimin  31376  ballotlem7  31406  subgrwlk  31989  cusgracyclt3v  32013  cvmlift2lem12  32171  fmlasucdisj  32256  dfon2lem8  32645  soseq  32707  segconeq  33082  ifscgr  33116  brofs2  33149  brifs2  33150  endofsegid  33157  dissneqlem  34173  rdgellim  34209  fvineqsneq  34245  tan2h  34436  matunitlindflem2  34441  poimirlem31  34475  poimir  34477  fzmul  34569  fdc  34573  incsequz2  34577  sstotbnd2  34605  sstotbnd3  34607  totbndbnd  34620  isexid2  34686  ispridl2  34869  mpobi123f  34993  riotasvd  35644  lsator0sp  35689  lssatle  35703  lshpset2N  35807  lkrlspeqN  35859  omllaw2N  35932  cmtbr3N  35942  lecmtN  35944  cvlcvr1  36027  cvrval4N  36102  cvrat3  36130  3noncolr2  36137  4noncolr3  36141  3dimlem3  36149  3dimlem3OLDN  36150  3dimlem4  36152  3dimlem4OLDN  36153  llncvrlpln  36246  lplncvrlvol  36304  snatpsubN  36438  linepsubN  36440  pmapjat1  36541  pclfinclN  36638  pl42N  36671  ltrneq2  36836  cdleme7aa  36930  cdleme18d  36983  cdleme21b  37014  trlord  37257  trlcoat  37411  dochkrshp  38074  lcfl8  38190  irrapxlem2  38926  pell14qrdich  38972  monotoddzz  39046  pw2f1ocnv  39140  iocinico  39324  nndomog  39403  harval3  39410  sbcim2g  40432  stoweidlem62  41911  elfzelfzlble  43059  eenglngeehlnmlem2  44228