Theorem sylbid 149

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylbid.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbid	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  nlimsucg  4481  poltletr  4939  xp11m  4977  fvmptdf  5508  elfvmptrab1  5515  eusvobj2  5760  ovmpodf  5902  f1o2ndf1  6125  smoiso  6199  nnsseleq  6397  ecopovtrn  6526  ecopovtrng  6529  dom2lem  6666  fundmen  6700  fidifsnen  6764  findcard2  6783  findcard2s  6784  supisoex  6896  infglbti  6912  ordiso2  6920  updjud  6967  difinfsnlem  6984  enomnilem  7010  addcanpig  7142  mulcanpig  7143  addnidpig  7144  ordpipqqs  7182  ltexnqq  7216  prarloclemlo  7302  genpcdl  7327  genpcuu  7328  mulnqprl  7376  mulnqpru  7377  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  distrlem5prl  7394  distrlem5pru  7395  ltsopr  7404  ltexprlemfl  7417  ltexprlemfu  7419  recexprlemss1l  7443  recexprlemss1u  7444  aptiprleml  7447  ltsrprg  7555  lttrsr  7570  mulextsr1lem  7588  axapti  7835  cnegexlem1  7937  le2add  8206  lt2add  8207  ltleadd  8208  lt2sub  8222  le2sub  8223  recexre  8340  reapti  8341  apreap  8349  reapcotr  8360  remulext1  8361  apreim  8365  apcotr  8369  mulext2  8375  recexap  8414  addltmul  8956  elnnz  9064  zleloe  9101  nn0n0n1ge2b  9130  nn0lt2  9132  nn0le2is012  9133  zextlt  9143  uzind2  9163  supinfneg  9390  infsupneg  9391  eluzdc  9404  qreccl  9434  xltnegi  9618  xnn0lenn0nn0  9648  iccid  9708  icoshft  9773  zltaddlt1le  9789  fzofzim  9965  qbtwnxr  10035  flqeqceilz  10091  modqmuladdnn0  10141  modfzo0difsn  10168  addmodlteq  10171  frec2uzrand  10178  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  facdiv  10484  facwordi  10486  faclbnd  10487  bcpasc  10512  seq3coll  10585  recvguniq  10767  abs00ap  10834  absext  10835  absnid  10845  cau3lem  10886  climuni  11062  2clim  11070  summodc  11152  fisumss  11161  fsumabs  11234  mertenslem2  11305  reeff1  11407  efieq1re  11478  dvdsmultr2  11533  dvdsleabs  11543  odd2np1lem  11569  odd2np1  11570  ltoddhalfle  11590  halfleoddlt  11591  m1expo  11597  nn0enne  11599  nn0ehalf  11600  nn0o1gt2  11602  flodddiv4  11631  zeqzmulgcd  11659  gcdneg  11670  gcdaddm  11672  bezoutlemaz  11691  bezoutlembz  11692  dfgcd2  11702  gcddiv  11707  dvdssqim  11712  algcvgblem  11730  algcvga  11732  lcmneg  11755  coprmgcdb  11769  coprmdvds2  11774  qredeq  11777  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  prmind2  11801  dvdsnprmd  11806  prmgt1  11812  nprmdvds1  11820  divgcdodd  11821  euclemma  11824  prmdvdsexpr  11828  prmfac1  11830  prmndvdsfaclt  11834  crth  11900  tgtop  12237  tgidm  12243  neipsm  12323  restbasg  12337  tgrest  12338  tgcn  12377  tgcnp  12378  cnconst2  12402  cnconst  12403  cnptopresti  12407  txbasval  12436  txcnp  12440  txdis1cn  12447  bldisj  12570  xblm  12586  blssps  12596  blss  12597  blin2  12601  cnlimcim  12809  dveflem  12855  sincosq3sgn  12909  sincosq4sgn  12910  coseq0q4123  12915  uzdcinzz  13005  subctctexmid  13196