Theorem sylibrd 262

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr4d  297  opeldmd  5887  elreldm  5916  predtrss  6325  ordtr2  6408  ssimaex  6970  fliftfun  7320  isopolem  7353  isosolem  7355  f1we  7363  ordsucss  7829  f1oweALT  7984  fnse  8150  soseq  8176  brtpos  8253  issmo2  8358  onelfvnef1  8450  seqomlem1  8461  omcl  8545  oecl  8546  oawordeulem  8563  oaass  8570  omordi  8575  omord  8577  odi  8588  oen0  8596  oeordi  8597  oeordsuc  8604  nnmcl  8622  nnecl  8623  nnmordi  8641  nnmord  8642  nnmwordri  8646  nnaordex  8648  swoord1  8751  ecopovtrn  8842  f1domg  8999  pw2f1olem  9101  domtriord  9143  mapen  9161  mapxpen  9163  mapunen  9166  nndomog  9229  onomeneq  9230  inficl  9418  supmo  9445  infmo  9490  inf3lem6  9635  cantnflem1  9691  tcmin  9741  tcrank  9902  cardne  10047  cardlim  10054  cardsdomel  10056  carduni  10063  alephord  10155  cardinfima  10177  dfac5lem4  10206  infdif2  10288  cofsmo  10348  cfcoflem  10351  infpssrlem4  10385  infpssrlem5  10386  fin4en1  10388  isfin2-2  10398  enfin2i  10400  fin23lem27  10407  isf32lem12  10443  isf34lem6  10459  domtriomlem  10521  cardmin  10649  fpwwe2lem11  10727  inar1  10861  gruiun  10885  ltsonq  11055  prub  11080  reclem3pr  11135  mulcmpblnr  11157  mulgt0sr  11191  axpre-sup  11255  leltadd  11801  infm3  12277  peano5nni  12339  zextle  12773  prime  12781  uzin  13002  ublbneg  13061  zbtwnre  13074  mul2lt0bi  13229  xrre2  13301  xralrple  13336  xmulneg1  13400  supxrbnd  13459  supxrgtmnf  13460  fzrevral  13747  flge  13946  ceile  13990  modadd1  14049  modmul1  14068  modsumfzodifsn  14088  seqcl2  14164  facdiv  14432  hashss  14554  hash2exprb  14617  elfzelfzccat  14726  repswswrd  14936  cshf1  14962  cshwcsh2id  14980  rlim2lt  15665  rlim3  15666  o1lo1  15705  climshftlem  15742  o1co  15754  o1of2  15781  isercolllem2  15834  isercoll  15836  caucvgrlem2  15843  climcndslem2  16020  sqrt2irr  16418  dvds2lem  16439  dvdsle  16481  dvdsfac  16497  ltoddhalfle  16532  divalglem0  16564  ndvdsadd  16581  bitsinv1lem  16612  sadcaddlem  16628  dvdslegcd  16675  bezoutlem2  16714  bezoutlem4  16716  gcdzeq  16726  algcvga  16755  rpdvds  16836  cncongr1  16843  cncongr2  16844  prmind2  16861  isprm6  16891  rpexp  16899  eulerthlem2  16960  pclem  17017  pceulem  17024  pc2dvds  17058  fldivp1  17076  infpnlem1  17089  prmunb  17093  mrieqv2d  17814  plttr  18515  clatl  18683  idressidex0  18861  issubg4  19357  gexdvds  19799  pgpssslw  19829  sylow2alem2  19833  efgs1b  19951  efgsfo  19954  imasabl  20091  lspindpi  21411  psgnodpm  21895  psgndif  21909  obselocv  22035  pf1ind  22674  mdetunilem9  22936  matunitlindflem2  22996  fiinbas  23271  bastg  23285  tgcl  23288  opnssneib  23434  clslp  23467  tgcnp  23572  iscnp4  23582  cncls2  23592  cncls  23593  cnntr  23594  cnpresti  23607  lmss  23617  lmcnp  23623  cmpsub  23719  tgcmp  23720  dfconn2  23738  t1connperf  23755  1stcfb  23764  1stcrest  23772  kgenss  23863  llycmpkgen2  23870  txdis  23952  qtoptop2  24019  kqt0lem  24056  isr0  24057  regr1lem2  24060  cmphaushmeo  24120  fbun  24160  ssfg  24192  fgtr  24210  ufildr  24251  cnpflf  24321  fclsnei  24339  flimfnfcls  24348  fclscmp  24350  ufilcmp  24352  cnpfcf  24361  alexsublem  24364  alexsubALTlem3  24369  alexsubALTlem4  24370  ptcmplem3  24374  tgphaus  24437  tgpt1  24438  tsmsres  24464  imasdsf1olem  24693  xblss2ps  24721  xblss2  24722  blsscls2  24824  metequiv2  24830  stdbdxmet  24835  nmoi  25048  reconn  25149  mulc1cncf  25227  cncfco  25229  iccpnfhmeo  25267  xrhmeo  25268  evth  25281  pi1grplem  25371  fgcfil  25593  ivthlem2  25774  ivthlem3  25775  ovolicc2lem4  25842  voliunlem1  25872  ioombl1lem4  25883  itg2gt0  26082  limcco  26214  lhop1  26335  tdeglem4  26379  plypf1  26532  coeeulem  26544  coeidlem  26557  coeid3  26560  plymul0or  26600  dvnply2  26609  plydivex  26619  plyconz  26632  vieta1lem2  26635  plyexmo  26637  aaliou3lem2  26671  ulmss  26725  ulmdvlem3  26730  iblulm  26735  sincosq2sgn  26829  sincosq3sgn  26830  sincosq4sgn  26831  logcnlem5  26975  dcubic  27175  amgm  27319  isnsqf  27463  mumullem2  27508  chtublem  27539  chtub  27540  fsumvma2  27542  vmasum  27544  dchrfi  27583  bposlem1  27612  bposlem3  27614  bposlem7  27618  lgsdir  27660  lgsquadlem2  27709  2sqlem8a  27753  2sqlem10  27756  dchrisum0flb  27838  pntpbnd1  27914  pntlemf  27933  pntlem3  27937  addonbday  28666  peano5uzs  28791  axeuclid  29542  uspgrushgr  29759  uspgrupgr  29760  usgruspgr  29762  subgrwlk  30270  usgr2pth  30351  crctcshwlkn0lem5  30404  wwlksnext  30483  wwlksnextsurj  30490  clwwlkccatlem  30581  clwlkclwwlkf  30600  clwwisshclwwslemlem  30605  lnon0  31401  normpyc  31749  ocsh  31886  ocorth  31894  ococss  31896  shsel2  31925  hsupss  31944  pjhth  31996  shlub  32017  cm2j  32223  lnfncnbd  32660  riesz1  32668  rnbra  32710  leopadd  32735  leopmuli  32736  hstles  32834  stge1i  32841  stle0i  32842  dmdbr5  32911  ssmd2  32915  superpos  32957  chcv1  32958  atoml2i  32986  chirredlem2  32994  atcvat3i  32999  mdsymlem5  33010  mdsymlem6  33011  sumdmdii  33018  sumdmdlem2  33022  isarchiofld  33803  sqsscirc2  34584  cnre2csqlem  34585  xrge0iifiso  34610  sigaclci  34807  omssubadd  34975  eulerpartlemb  35043  ballotlemimin  35181  ballotlem7  35211  fineqvac  35833  fineqvinfep  35842  j0ltaleph  35940  vonf1wev  35948  vonf1owevOLD  35950  cusgracyclt3v  35990  cvmlift2lem12  36148  fmlasucdisj  36233  dfon2lem8  36627  segconeq  36850  ifscgr  36884  brofs2  36917  brifs2  36918  endofsegid  36925  ltnmul  37040  dissneqlem  38339  rdgellim  38375  fvineqsneq  38411  tan2h  38611  poimirlem31  38645  poimir  38647  fzmul  38751  fdc  38755  incsequz2  38759  sstotbnd2  38784  sstotbnd3  38786  totbndbnd  38799  isexid2  38865  ispridl2  39048  mpobi123f  39170  disjlem18  39911  disjdmqsss  39913  eldisjs6  39948  riotasvd  40089  lsator0sp  40134  lssatle  40148  lshpset2N  40252  lkrlspeqN  40304  omllaw2N  40377  cmtbr3N  40387  lecmtN  40389  cvlcvr1  40472  cvrval4N  40547  cvrat3  40575  3noncolr2  40582  4noncolr3  40586  3dimlem3  40594  3dimlem3OLDN  40595  3dimlem4  40597  3dimlem4OLDN  40598  llncvrlpln  40691  lplncvrlvol  40749  snatpsubN  40883  linepsubN  40885  pmapjat1  40986  pclfinclN  41083  pl42N  41116  ltrneq2  41281  cdleme7aa  41375  cdleme18d  41428  cdleme21b  41459  trlord  41702  trlcoat  41856  dochkrshp  42519  lcfl8  42635  mulgt0con1dlem  43609  irrapxlem2  43906  pell14qrdich  43952  monotoddzz  44026  pw2f1ocnv  44120  iocinico  44290  ordnexbtwnsuc  44345  tfsconcat0i  44423  naddwordnexlem4  44479  harval3  44615  sbcim2g  45597  stoweidlem62  47148  elfzelfzlble  48467  pgnbgreunbgrlem1  49287  pgnbgreunbgrlem4  49293  1arymaptf1  49830  2arymaptf1  49841  eenglngeehlnmlem2  49926  mpbiran3d  49983  opnneil  50094