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  3829  opeldmd  5919  elreldm  5948  predtrss  6344  ordtr2  6429  ssimaex  6993  fliftfun  7331  isopolem  7364  isosolem  7366  ordsucss  7837  f1oweALT  7995  fnse  8156  soseq  8182  brtpos  8258  issmo2  8387  seqomlem1  8488  omcl  8572  oecl  8573  oawordeulem  8590  oaass  8597  omordi  8602  omord  8604  odi  8615  oen0  8622  oeordi  8623  oeordsuc  8630  nnmcl  8648  nnecl  8649  nnmordi  8667  nnmord  8668  nnmwordri  8672  nnaordex  8674  swoord1  8775  ecopovtrn  8858  f1domg  9010  pw2f1olem  9114  domtriord  9161  mapen  9179  mapxpen  9181  mapunen  9184  nndomog  9250  nndomogOLD  9260  onomeneq  9262  inficl  9462  supmo  9489  infmo  9532  inf3lem6  9670  cantnflem1  9726  tcmin  9778  tcrank  9921  cardne  10002  cardlim  10009  cardsdomel  10011  carduni  10018  alephord  10112  cardinfima  10134  dfac5lem4  10163  dfac5lem4OLD  10165  infdif2  10246  cofsmo  10306  cfcoflem  10309  infpssrlem4  10343  infpssrlem5  10344  fin4en1  10346  isfin2-2  10356  enfin2i  10358  fin23lem27  10365  isf32lem12  10401  isf34lem6  10417  domtriomlem  10479  cardmin  10601  fpwwe2lem11  10678  inar1  10812  gruiun  10836  ltsonq  11006  prub  11031  reclem3pr  11086  mulcmpblnr  11108  mulgt0sr  11142  axpre-sup  11206  leltadd  11744  infm3  12224  peano5nni  12266  zextle  12688  prime  12696  uzin  12915  ublbneg  12972  zbtwnre  12985  mul2lt0bi  13138  xrre2  13208  xralrple  13243  xmulneg1  13307  supxrbnd  13366  supxrgtmnf  13367  fzrevral  13648  flge  13841  ceile  13885  modadd1  13944  modmul1  13961  modsumfzodifsn  13981  seqcl2  14057  facdiv  14322  hashss  14444  hash2exprb  14506  elfzelfzccat  14614  repswswrd  14818  cshf1  14844  cshwcsh2id  14863  rlim2lt  15529  rlim3  15530  o1lo1  15569  climshftlem  15606  o1co  15618  o1of2  15645  isercolllem2  15698  isercoll  15700  caucvgrlem2  15707  climcndslem2  15882  sqrt2irr  16281  dvds2lem  16302  dvdsle  16343  dvdsfac  16359  ltoddhalfle  16394  divalglem0  16426  ndvdsadd  16443  bitsinv1lem  16474  sadcaddlem  16490  dvdslegcd  16537  bezoutlem2  16573  bezoutlem4  16575  gcdzeq  16585  algcvga  16612  rpdvds  16693  cncongr1  16700  cncongr2  16701  prmind2  16718  isprm6  16747  rpexp  16755  eulerthlem2  16815  pclem  16871  pceulem  16878  pc2dvds  16912  fldivp1  16930  infpnlem1  16943  prmunb  16947  mrieqv2d  17683  plttr  18399  clatl  18565  issubg4  19175  gexdvds  19616  pgpssslw  19646  sylow2alem2  19650  efgs1b  19768  efgsfo  19771  imasabl  19908  lspindpi  21151  psgnodpm  21623  psgndif  21637  obselocv  21765  pf1ind  22374  mdetunilem9  22641  fiinbas  22974  bastg  22988  tgcl  22991  opnssneib  23138  clslp  23171  tgcnp  23276  iscnp4  23286  cncls2  23296  cncls  23297  cnntr  23298  cnpresti  23311  lmss  23321  lmcnp  23327  cmpsub  23423  tgcmp  23424  dfconn2  23442  t1connperf  23459  1stcfb  23468  1stcrest  23476  kgenss  23566  llycmpkgen2  23573  txdis  23655  qtoptop2  23722  kqt0lem  23759  isr0  23760  regr1lem2  23763  cmphaushmeo  23823  fbun  23863  ssfg  23895  fgtr  23913  ufildr  23954  cnpflf  24024  fclsnei  24042  flimfnfcls  24051  fclscmp  24053  ufilcmp  24055  cnpfcf  24064  alexsublem  24067  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem3  24077  tgphaus  24140  tgpt1  24141  tsmsres  24167  imasdsf1olem  24398  xblss2ps  24426  xblss2  24427  blsscls2  24532  metequiv2  24538  stdbdxmet  24543  nmoi  24764  reconn  24863  mulc1cncf  24944  cncfco  24946  iccpnfhmeo  24989  xrhmeo  24990  evth  25004  pi1grplem  25095  fgcfil  25318  ivthlem2  25500  ivthlem3  25501  ovolicc2lem4  25568  voliunlem1  25598  ioombl1lem4  25609  itg2gt0  25809  limcco  25942  lhop1  26067  tdeglem4  26113  plypf1  26265  coeeulem  26277  coeidlem  26290  coeid3  26293  plymul0or  26336  dvnply2  26343  plydivex  26353  vieta1lem2  26367  plyexmo  26369  aaliou3lem2  26399  ulmss  26454  ulmdvlem3  26459  iblulm  26464  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  logcnlem5  26702  dcubic  26903  amgm  27048  isnsqf  27192  mumullem2  27237  chtublem  27269  chtub  27270  fsumvma2  27272  vmasum  27274  dchrfi  27313  bposlem1  27342  bposlem3  27344  bposlem7  27348  lgsdir  27390  lgsquadlem2  27439  2sqlem8a  27483  2sqlem10  27486  dchrisum0flb  27568  pntpbnd1  27644  pntlemf  27663  pntlem3  27667  peano5uzs  28404  axeuclid  28992  uspgrushgr  29208  uspgrupgr  29209  usgruspgr  29211  usgr2pth  29796  crctcshwlkn0lem5  29843  wwlksnext  29922  wwlksnextsurj  29929  clwwlkccatlem  30017  clwlkclwwlkf  30036  clwwisshclwwslemlem  30041  lnon0  30826  normpyc  31174  ocsh  31311  ocorth  31319  ococss  31321  shsel2  31350  hsupss  31369  pjhth  31421  shlub  31442  cm2j  31648  lnfncnbd  32085  riesz1  32093  rnbra  32135  leopadd  32160  leopmuli  32161  hstles  32259  stge1i  32266  stle0i  32267  dmdbr5  32336  ssmd2  32340  superpos  32382  chcv1  32383  atoml2i  32411  chirredlem2  32419  atcvat3i  32424  mdsymlem5  32435  mdsymlem6  32436  sumdmdii  32443  sumdmdlem2  32447  isarchiofld  33326  sqsscirc2  33869  cnre2csqlem  33870  xrge0iifiso  33895  sigaclci  34112  omssubadd  34281  eulerpartlemb  34349  ballotlemimin  34486  ballotlem7  34516  fineqvac  35089  subgrwlk  35116  cusgracyclt3v  35140  cvmlift2lem12  35298  fmlasucdisj  35383  dfon2lem8  35771  segconeq  35991  ifscgr  36025  brofs2  36058  brifs2  36059  endofsegid  36066  dissneqlem  37322  rdgellim  37358  fvineqsneq  37394  tan2h  37598  matunitlindflem2  37603  poimirlem31  37637  poimir  37639  fzmul  37727  fdc  37731  incsequz2  37735  sstotbnd2  37760  sstotbnd3  37762  totbndbnd  37775  isexid2  37841  ispridl2  38024  mpobi123f  38148  disjlem18  38781  disjdmqsss  38783  riotasvd  38937  lsator0sp  38982  lssatle  38996  lshpset2N  39100  lkrlspeqN  39152  omllaw2N  39225  cmtbr3N  39235  lecmtN  39237  cvlcvr1  39320  cvrval4N  39396  cvrat3  39424  3noncolr2  39431  4noncolr3  39435  3dimlem3  39443  3dimlem3OLDN  39444  3dimlem4  39446  3dimlem4OLDN  39447  llncvrlpln  39540  lplncvrlvol  39598  snatpsubN  39732  linepsubN  39734  pmapjat1  39835  pclfinclN  39932  pl42N  39965  ltrneq2  40130  cdleme7aa  40224  cdleme18d  40277  cdleme21b  40308  trlord  40551  trlcoat  40705  dochkrshp  41368  lcfl8  41484  mulgt0con1dlem  42463  irrapxlem2  42810  pell14qrdich  42856  monotoddzz  42931  pw2f1ocnv  43025  iocinico  43200  ordnexbtwnsuc  43256  tfsconcat0i  43334  naddwordnexlem4  43390  harval3  43527  sbcim2g  44535  stoweidlem62  46017  elfzelfzlble  47270  1arymaptf1  48491  2arymaptf1  48502  eenglngeehlnmlem2  48587  mpbiran3d  48645  opnneil  48705