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  3777  opeldmd  5844  elreldm  5872  predtrss  6265  ordtr2  6347  ssimaex  6902  fliftfun  7241  isopolem  7274  isosolem  7276  ordsucss  7743  f1oweALT  7899  fnse  8058  soseq  8084  brtpos  8160  issmo2  8264  seqomlem1  8364  omcl  8446  oecl  8447  oawordeulem  8464  oaass  8471  omordi  8476  omord  8478  odi  8489  oen0  8496  oeordi  8497  oeordsuc  8504  nnmcl  8522  nnecl  8523  nnmordi  8541  nnmord  8542  nnmwordri  8546  nnaordex  8548  swoord1  8649  ecopovtrn  8739  f1domg  8889  pw2f1olem  8989  domtriord  9031  mapen  9049  mapxpen  9051  mapunen  9054  nndomog  9117  onomeneq  9118  inficl  9304  supmo  9331  infmo  9376  inf3lem6  9518  cantnflem1  9574  tcmin  9626  tcrank  9769  cardne  9850  cardlim  9857  cardsdomel  9859  carduni  9866  alephord  9958  cardinfima  9980  dfac5lem4  10009  dfac5lem4OLD  10011  infdif2  10092  cofsmo  10152  cfcoflem  10155  infpssrlem4  10189  infpssrlem5  10190  fin4en1  10192  isfin2-2  10202  enfin2i  10204  fin23lem27  10211  isf32lem12  10247  isf34lem6  10263  domtriomlem  10325  cardmin  10447  fpwwe2lem11  10524  inar1  10658  gruiun  10682  ltsonq  10852  prub  10877  reclem3pr  10932  mulcmpblnr  10954  mulgt0sr  10988  axpre-sup  11052  leltadd  11593  infm3  12073  peano5nni  12120  zextle  12538  prime  12546  uzin  12764  ublbneg  12823  zbtwnre  12836  mul2lt0bi  12990  xrre2  13061  xralrple  13096  xmulneg1  13160  supxrbnd  13219  supxrgtmnf  13220  fzrevral  13504  flge  13701  ceile  13745  modadd1  13804  modmul1  13823  modsumfzodifsn  13843  seqcl2  13919  facdiv  14186  hashss  14308  hash2exprb  14370  elfzelfzccat  14479  repswswrd  14683  cshf1  14709  cshwcsh2id  14727  rlim2lt  15396  rlim3  15397  o1lo1  15436  climshftlem  15473  o1co  15485  o1of2  15512  isercolllem2  15565  isercoll  15567  caucvgrlem2  15574  climcndslem2  15749  sqrt2irr  16150  dvds2lem  16171  dvdsle  16213  dvdsfac  16229  ltoddhalfle  16264  divalglem0  16296  ndvdsadd  16313  bitsinv1lem  16344  sadcaddlem  16360  dvdslegcd  16407  bezoutlem2  16443  bezoutlem4  16445  gcdzeq  16455  algcvga  16482  rpdvds  16563  cncongr1  16570  cncongr2  16571  prmind2  16588  isprm6  16617  rpexp  16625  eulerthlem2  16685  pclem  16742  pceulem  16749  pc2dvds  16783  fldivp1  16801  infpnlem1  16814  prmunb  16818  mrieqv2d  17537  plttr  18238  clatl  18406  issubg4  19050  gexdvds  19489  pgpssslw  19519  sylow2alem2  19523  efgs1b  19641  efgsfo  19644  imasabl  19781  lspindpi  21062  psgnodpm  21518  psgndif  21532  obselocv  21658  pf1ind  22263  mdetunilem9  22528  fiinbas  22860  bastg  22874  tgcl  22877  opnssneib  23023  clslp  23056  tgcnp  23161  iscnp4  23171  cncls2  23181  cncls  23182  cnntr  23183  cnpresti  23196  lmss  23206  lmcnp  23212  cmpsub  23308  tgcmp  23309  dfconn2  23327  t1connperf  23344  1stcfb  23353  1stcrest  23361  kgenss  23451  llycmpkgen2  23458  txdis  23540  qtoptop2  23607  kqt0lem  23644  isr0  23645  regr1lem2  23648  cmphaushmeo  23708  fbun  23748  ssfg  23780  fgtr  23798  ufildr  23839  cnpflf  23909  fclsnei  23927  flimfnfcls  23936  fclscmp  23938  ufilcmp  23940  cnpfcf  23949  alexsublem  23952  alexsubALTlem3  23957  alexsubALTlem4  23958  ptcmplem3  23962  tgphaus  24025  tgpt1  24026  tsmsres  24052  imasdsf1olem  24281  xblss2ps  24309  xblss2  24310  blsscls2  24412  metequiv2  24418  stdbdxmet  24423  nmoi  24636  reconn  24737  mulc1cncf  24818  cncfco  24820  iccpnfhmeo  24863  xrhmeo  24864  evth  24878  pi1grplem  24969  fgcfil  25191  ivthlem2  25373  ivthlem3  25374  ovolicc2lem4  25441  voliunlem1  25471  ioombl1lem4  25482  itg2gt0  25681  limcco  25814  lhop1  25939  tdeglem4  25985  plypf1  26137  coeeulem  26149  coeidlem  26162  coeid3  26165  plymul0or  26208  dvnply2  26215  plydivex  26225  vieta1lem2  26239  plyexmo  26241  aaliou3lem2  26271  ulmss  26326  ulmdvlem3  26331  iblulm  26336  sincosq2sgn  26428  sincosq3sgn  26429  sincosq4sgn  26430  logcnlem5  26575  dcubic  26776  amgm  26921  isnsqf  27065  mumullem2  27110  chtublem  27142  chtub  27143  fsumvma2  27145  vmasum  27147  dchrfi  27186  bposlem1  27215  bposlem3  27217  bposlem7  27221  lgsdir  27263  lgsquadlem2  27312  2sqlem8a  27356  2sqlem10  27359  dchrisum0flb  27441  pntpbnd1  27517  pntlemf  27536  pntlem3  27540  peano5uzs  28321  axeuclid  28934  uspgrushgr  29148  uspgrupgr  29149  usgruspgr  29151  usgr2pth  29735  crctcshwlkn0lem5  29785  wwlksnext  29864  wwlksnextsurj  29871  clwwlkccatlem  29959  clwlkclwwlkf  29978  clwwisshclwwslemlem  29983  lnon0  30768  normpyc  31116  ocsh  31253  ocorth  31261  ococss  31263  shsel2  31292  hsupss  31311  pjhth  31363  shlub  31384  cm2j  31590  lnfncnbd  32027  riesz1  32035  rnbra  32077  leopadd  32102  leopmuli  32103  hstles  32201  stge1i  32208  stle0i  32209  dmdbr5  32278  ssmd2  32282  superpos  32324  chcv1  32325  atoml2i  32353  chirredlem2  32361  atcvat3i  32366  mdsymlem5  32377  mdsymlem6  32378  sumdmdii  32385  sumdmdlem2  32389  isarchiofld  33158  sqsscirc2  33912  cnre2csqlem  33913  xrge0iifiso  33938  sigaclci  34135  omssubadd  34303  eulerpartlemb  34371  ballotlemimin  34509  ballotlem7  34539  fineqvac  35107  vonf1owev  35120  subgrwlk  35144  cusgracyclt3v  35168  cvmlift2lem12  35326  fmlasucdisj  35411  dfon2lem8  35803  segconeq  36023  ifscgr  36057  brofs2  36090  brifs2  36091  endofsegid  36098  dissneqlem  37353  rdgellim  37389  fvineqsneq  37425  tan2h  37631  matunitlindflem2  37636  poimirlem31  37670  poimir  37672  fzmul  37760  fdc  37764  incsequz2  37768  sstotbnd2  37793  sstotbnd3  37795  totbndbnd  37808  isexid2  37874  ispridl2  38057  mpobi123f  38181  disjlem18  38817  disjdmqsss  38819  riotasvd  38974  lsator0sp  39019  lssatle  39033  lshpset2N  39137  lkrlspeqN  39189  omllaw2N  39262  cmtbr3N  39272  lecmtN  39274  cvlcvr1  39357  cvrval4N  39432  cvrat3  39460  3noncolr2  39467  4noncolr3  39471  3dimlem3  39479  3dimlem3OLDN  39480  3dimlem4  39482  3dimlem4OLDN  39483  llncvrlpln  39576  lplncvrlvol  39634  snatpsubN  39768  linepsubN  39770  pmapjat1  39871  pclfinclN  39968  pl42N  40001  ltrneq2  40166  cdleme7aa  40260  cdleme18d  40313  cdleme21b  40344  trlord  40587  trlcoat  40741  dochkrshp  41404  lcfl8  41520  mulgt0con1dlem  42481  irrapxlem2  42835  pell14qrdich  42881  monotoddzz  42955  pw2f1ocnv  43049  iocinico  43224  ordnexbtwnsuc  43279  tfsconcat0i  43357  naddwordnexlem4  43413  harval3  43550  sbcim2g  44550  stoweidlem62  46079  elfzelfzlble  47331  pgnbgreunbgrlem1  48123  pgnbgreunbgrlem4  48129  1arymaptf1  48653  2arymaptf1  48664  eenglngeehlnmlem2  48749  mpbiran3d  48807  opnneil  48920