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  4551  poltletr  5013  xp11m  5051  fvmptdf  5587  elfvmptrab1  5594  eusvobj2  5843  ovmpodf  5988  f1o2ndf1  6211  smoiso  6285  nnsseleq  6484  ecopovtrn  6614  ecopovtrng  6617  dom2lem  6754  fundmen  6788  fidifsnen  6852  findcard2  6871  findcard2s  6872  supisoex  6990  infglbti  7006  ordiso2  7016  updjud  7063  difinfsnlem  7080  enomnilem  7118  enmkvlem  7141  cc2lem  7232  addcanpig  7300  mulcanpig  7301  addnidpig  7302  ordpipqqs  7340  ltexnqq  7374  prarloclemlo  7460  genpcdl  7485  genpcuu  7486  mulnqprl  7534  mulnqpru  7535  distrlem1prl  7548  distrlem1pru  7549  distrlem4prl  7550  distrlem4pru  7551  distrlem5prl  7552  distrlem5pru  7553  ltsopr  7562  ltexprlemfl  7575  ltexprlemfu  7577  recexprlemss1l  7601  recexprlemss1u  7602  aptiprleml  7605  ltsrprg  7713  lttrsr  7728  mulextsr1lem  7746  axapti  7994  cnegexlem1  8098  le2add  8367  lt2add  8368  ltleadd  8369  lt2sub  8383  le2sub  8384  recexre  8501  reapti  8502  apreap  8510  reapcotr  8521  remulext1  8522  apreim  8526  apcotr  8530  mulext2  8536  recexap  8575  addltmul  9118  elnnz  9226  zleloe  9263  difgtsumgt  9285  nn0n0n1ge2b  9295  nn0lt2  9297  nn0le2is012  9298  zextlt  9308  uzind2  9328  supinfneg  9558  infsupneg  9559  eluzdc  9573  qreccl  9605  elpq  9611  xltnegi  9796  xnn0lenn0nn0  9826  iccid  9886  icoshft  9951  zltaddlt1le  9968  fzofzim  10148  qbtwnxr  10218  flqeqceilz  10278  modqmuladdnn0  10328  modfzo0difsn  10355  addmodlteq  10358  frec2uzrand  10365  frecuzrdgtcl  10372  frecuzrdgfunlem  10379  facdiv  10676  facwordi  10678  faclbnd  10679  bcpasc  10704  seq3coll  10781  recvguniq  10963  abs00ap  11030  absext  11031  absnid  11041  cau3lem  11082  climuni  11260  2clim  11268  summodc  11350  fisumss  11359  fsumabs  11432  mertenslem2  11503  fprodssdc  11557  reeff1  11667  efieq1re  11738  dvdsmultr2  11799  dvdsleabs  11809  odd2np1lem  11835  odd2np1  11836  ltoddhalfle  11856  halfleoddlt  11857  m1expo  11863  nn0enne  11865  nn0ehalf  11866  nn0o1gt2  11868  flodddiv4  11897  zeqzmulgcd  11929  gcdneg  11941  gcdaddm  11943  bezoutlemaz  11962  bezoutlembz  11963  dfgcd2  11973  gcddiv  11978  dvdssqim  11983  algcvgblem  12007  algcvga  12009  lcmneg  12032  coprmgcdb  12046  coprmdvds2  12051  qredeq  12054  divgcdcoprm0  12059  divgcdcoprmex  12060  cncongr1  12061  cncongr2  12062  prmind2  12078  dvdsnprmd  12083  prmgt1  12090  nprmdvds1  12098  divgcdodd  12101  euclemma  12104  prmdvdsexpr  12108  prmfac1  12110  prmndvdsfaclt  12114  crth  12182  eulerthlemh  12189  fermltl  12192  nnnn0modprm0  12213  coprimeprodsq2  12216  pythagtriplem2  12224  pcpremul  12251  pcdvdsb  12277  pc2dvds  12287  pc11  12288  dvdsprmpweqnn  12293  dvdsprmpweqle  12294  difsqpwdvds  12295  pcfac  12306  oddprmdvds  12310  prmpwdvds  12311  1arith  12323  grp1inv  12810  tgtop  12947  tgidm  12953  neipsm  13033  restbasg  13047  tgrest  13048  tgcn  13087  tgcnp  13088  cnconst2  13112  cnconst  13113  cnptopresti  13117  txbasval  13146  txcnp  13150  txdis1cn  13157  bldisj  13280  xblm  13296  blssps  13306  blss  13307  blin2  13311  cnlimcim  13519  dveflem  13566  sincosq3sgn  13628  sincosq4sgn  13629  coseq0q4123  13634  ioocosf1o  13654  logbgcd1irr  13764  zabsle1  13779  lgsdir2lem5  13812  lgsne0  13818  lgsdirnn0  13827  uzdcinzz  13918  subctctexmid  14119