Theorem sylibd 149

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

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  dvelimdf  2069  ceqsalt  2829  sbceqal  3087  csbiebt  3167  rspcsbela  3187  preqr1g  3849  repizf2  4252  copsexg  4336  onun2  4588  suc11g  4655  elrnrexdm  5786  isoselem  5961  riotass2  6000  oawordriexmid  6638  nnm00  6698  ecopovtrn  6801  ecopovtrng  6804  infglbti  7224  difinfsnlem  7298  enq0tr  7654  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  mulextsr1lem  8000  pitonn  8068  rereceu  8109  cnegexlem1  8354  ltadd2  8599  eqord2  8664  mulext  8794  mulgt1  9043  lt2halves  9380  addltmul  9381  nzadd  9532  ltsubnn0  9547  zextlt  9572  recnz  9573  zeo  9585  peano5uzti  9588  irradd  9880  irrmul  9881  xltneg  10071  xleadd1  10110  icc0r  10161  fznuz  10337  uznfz  10338  facndiv  11002  ccatalpha  11191  swrdccatin2  11311  swrdccatin2d  11326  rennim  11564  abs00ap  11624  absle  11651  cau3lem  11676  caubnd2  11679  climshft  11866  subcn2  11873  mulcn2  11874  serf0  11914  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  efieq1re  12335  moddvds  12362  dvdsssfz1  12415  nn0seqcvgd  12615  algcvgblem  12623  eucalglt  12631  lcmgcdlem  12651  rpmul  12672  divgcdcoprm0  12675  isprm6  12721  rpexp  12727  eulerthlema  12804  eulerthlemh  12805  prmdiv  12809  pcprendvds2  12866  pcz  12907  pcprmpw  12909  pcadd2  12916  pcfac  12925  expnprm  12928  imasgrp2  13699  issubg4m  13782  znidomb  14675  tgss3  14805  cnpnei  14946  cnntr  14952  hmeoopn  15038  hmeocld  15039  mulcncflem  15334  plycolemc  15485  sincosq3sgn  15555  sincosq4sgn  15556  perfect1  15725  lgsdir2lem4  15763  lgsne0  15770  lgsquad2lem2  15814  2sqlem8a  15854  clwwlkext2edg  16276  bj-peano4  16571  iswomni0  16676