Theorem sylibrd 248

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3imtr4d  282  sbciegft  3433  eqsbc3rOLD  3460  opeldmd  5249  elreldm  5271  ordtr2  5685  ssimaex  6173  fliftfun  6462  isopolem  6495  isosolem  6497  ordsucss  6910  f1oweALT  7043  fnse  7181  brtpos  7248  issmo2  7333  seqomlem1  7432  omcl  7503  oecl  7504  oawordeulem  7521  oaass  7528  omordi  7533  omord  7535  odi  7546  oen0  7553  oeordi  7554  oeordsuc  7561  nnmcl  7579  nnecl  7580  nnmordi  7598  nnmord  7599  nnmwordri  7603  nnaordex  7605  swoord1  7660  ecopovtrn  7737  f1domg  7861  pw2f1olem  7949  domtriord  7991  mapen  8009  mapxpen  8011  mapunen  8014  nndomo  8039  inficl  8214  supmo  8241  infmo  8284  inf3lem6  8413  cantnflem1  8469  tcmin  8500  tcrank  8630  cardne  8674  cardlim  8681  cardsdomel  8683  carduni  8690  alephord  8781  cardinfima  8803  dfac5lem4  8832  infdif2  8915  cofsmo  8974  cfcoflem  8977  infpssrlem4  9011  infpssrlem5  9012  fin4en1  9014  isfin2-2  9024  enfin2i  9026  fin23lem27  9033  isf32lem12  9069  isf34lem6  9085  domtriomlem  9147  cardmin  9265  fpwwe2lem12  9342  inar1  9476  gruiun  9500  ltsonq  9670  prub  9695  reclem3pr  9750  mulcmpblnr  9771  mulgt0sr  9805  axpre-sup  9869  leltadd  10391  infm3  10861  peano5nni  10900  zextle  11326  prime  11334  uzin  11596  ublbneg  11649  zbtwnre  11662  mul2lt0bi  11812  xrre2  11875  xralrple  11910  xmulneg1  11971  supxrbnd  12030  supxrgtmnf  12031  fzrevral  12294  flge  12468  ceile  12510  modadd1  12569  modmul1  12585  modsumfzodifsn  12605  seqcl2  12681  facdiv  12936  hashss  13058  hash2exprb  13110  elfzelfzccat  13217  repswswrd  13382  cshf1  13407  cshwcsh2id  13425  rlim2lt  14076  rlim3  14077  o1lo1  14116  climshftlem  14153  o1co  14165  o1of2  14191  isercolllem2  14244  isercoll  14246  caucvgrlem2  14253  climcndslem2  14421  sqrt2irr  14817  dvds2lem  14832  dvdsle  14870  dvdsfac  14886  ltoddhalfle  14923  divalglem0  14954  ndvdsadd  14972  bitsinv1lem  15001  sadcaddlem  15017  dvdslegcd  15064  bezoutlem2  15095  bezoutlem4  15097  gcdzeq  15109  algcvga  15130  rpdvds  15212  cncongr1  15219  cncongr2  15220  prmind2  15236  isprm6  15264  rpexp  15270  eulerthlem2  15325  pclem  15381  pceulem  15388  pc2dvds  15421  fldivp1  15439  infpnlem1  15452  prmunb  15456  mrieqv2d  16122  plttr  16793  clatl  16939  issubg4  17436  gexdvds  17822  pgpssslw  17852  sylow2alem2  17856  efgs1b  17972  efgsfo  17975  lspindpi  18953  pf1ind  19540  psgnodpm  19753  psgndif  19767  obselocv  19891  mdetunilem9  20245  fiinbas  20567  bastg  20581  tgcl  20584  opnssneib  20729  clslp  20762  tgcnp  20867  iscnp4  20877  cncls2  20887  cncls  20888  cnntr  20889  cnpresti  20902  lmss  20912  lmcnp  20918  cmpsub  21013  tgcmp  21014  dfcon2  21032  t1conperf  21049  1stcfb  21058  1stcrest  21066  kgenss  21156  llycmpkgen2  21163  txdis  21245  qtoptop2  21312  kqt0lem  21349  isr0  21350  regr1lem2  21353  cmphaushmeo  21413  fbun  21454  ssfg  21486  fgtr  21504  ufildr  21545  cnpflf  21615  fclsnei  21633  flimfnfcls  21642  fclscmp  21644  ufilcmp  21646  cnpfcf  21655  alexsublem  21658  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem3  21668  tgphaus  21730  tgpt1  21731  tsmsres  21757  imasdsf1olem  21988  xblss2ps  22016  xblss2  22017  blsscls2  22119  metequiv2  22125  stdbdxmet  22130  nmoi  22342  reconn  22439  mulc1cncf  22516  cncfco  22518  iccpnfhmeo  22552  xrhmeo  22553  evth  22566  pi1grplem  22657  fgcfil  22877  ivthlem2  23028  ivthlem3  23029  ovolicc2lem4  23095  voliunlem1  23125  ioombl1lem4  23136  itg2gt0  23333  limcco  23463  lhop1  23581  tdeglem4  23624  plypf1  23772  coeeulem  23784  coeidlem  23797  coeid3  23800  plymul0or  23840  dvnply2  23846  plydivex  23856  vieta1lem2  23870  plyexmo  23872  aaliou3lem2  23902  ulmss  23955  ulmdvlem3  23960  iblulm  23965  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  logcnlem5  24192  dcubic  24373  amgm  24517  isnsqf  24661  mumullem2  24706  chtublem  24736  chtub  24737  fsumvma2  24739  vmasum  24741  dchrfi  24780  bposlem1  24809  bposlem3  24811  bposlem7  24815  lgsdir  24857  lgsquadlem2  24906  2sqlem8a  24950  2sqlem10  24953  dchrisum0flb  24999  pntpbnd1  25075  pntlemf  25094  pntlem3  25098  axeuclid  25643  umisuhgra  25856  uslisushgra  25892  uslisumgra  25893  usisuslgra  25894  constr3trl  26187  constr3pth  26188  wwlknext  26252  wwlkextsur  26259  clwwisshclwwlem1  26333  vdusgraval  26434  lnon0  27037  normpyc  27387  ocsh  27526  ocorth  27534  ococss  27536  shsel2  27565  hsupss  27584  pjhth  27636  shlub  27657  cm2j  27863  lnfncnbd  28300  riesz1  28308  rnbra  28350  leopadd  28375  leopmuli  28376  hstles  28474  stge1i  28481  stle0i  28482  dmdbr5  28551  ssmd2  28555  superpos  28597  chcv1  28598  atoml2i  28626  chirredlem2  28634  atcvat3i  28639  mdsymlem5  28650  mdsymlem6  28651  sumdmdii  28658  sumdmdlem2  28662  isarchiofld  29148  sqsscirc2  29283  cnre2csqlem  29284  xrge0iifiso  29309  sigaclci  29522  omssubadd  29689  eulerpartlemb  29757  ballotlemimin  29894  ballotlem7  29924  cvmlift2lem12  30550  dfon2lem8  30939  soseq  30995  segconeq  31287  ifscgr  31321  brofs2  31354  brifs2  31355  endofsegid  31362  dissneqlem  32363  tan2h  32571  matunitlindflem2  32576  poimirlem31  32610  poimir  32612  fzmul  32707  fdc  32711  incsequz2  32715  sstotbnd2  32743  sstotbnd3  32745  totbndbnd  32758  isexid2  32824  ispridl2  33007  mpt2bi123f  33141  riotasvd  33260  lsator0sp  33306  lssatle  33320  lshpset2N  33424  lkrlspeqN  33476  omllaw2N  33549  cmtbr3N  33559  lecmtN  33561  cvlcvr1  33644  cvrval4N  33718  cvrat3  33746  3noncolr2  33753  4noncolr3  33757  3dimlem3  33765  3dimlem3OLDN  33766  3dimlem4  33768  3dimlem4OLDN  33769  llncvrlpln  33862  lplncvrlvol  33920  snatpsubN  34054  linepsubN  34056  pmapjat1  34157  pclfinclN  34254  pl42N  34287  ltrneq2  34452  cdleme7aa  34547  cdleme18d  34600  cdleme21b  34632  trlord  34875  trlcoat  35029  dochkrshp  35693  lcfl8  35809  irrapxlem2  36405  pell14qrdich  36451  monotoddzz  36526  pw2f1ocnv  36622  iocinico  36816  sbcim2g  37769  stoweidlem62  38955  elfzelfzlble  40358  uspgrushgr  40405  uspgrupgr  40406  usgruspgr  40408  crctcsh1wlkn0lem5  41017  wwlksnext  41099  wwlksnextsur  41106  clwwisshclwwslemlem  41233