Theorem sylibd 148

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 143	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 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:  3imtr3d  201  dvelimdf  2004  ceqsalt  2751  sbceqal  3005  csbiebt  3083  rspcsbela  3103  preqr1g  3745  repizf2  4140  copsexg  4221  onun2  4466  suc11g  4533  elrnrexdm  5623  isoselem  5787  riotass2  5823  oawordriexmid  6434  nnm00  6493  ecopovtrn  6594  ecopovtrng  6597  infglbti  6986  difinfsnlem  7060  enq0tr  7371  addnqprl  7466  addnqpru  7467  mulnqprl  7505  mulnqpru  7506  recexprlemss1l  7572  recexprlemss1u  7573  cauappcvgprlemdisj  7588  mulextsr1lem  7717  pitonn  7785  rereceu  7826  cnegexlem1  8069  ltadd2  8313  eqord2  8378  mulext  8508  mulgt1  8754  lt2halves  9088  addltmul  9089  nzadd  9239  ltsubnn0  9254  zextlt  9279  recnz  9280  zeo  9292  peano5uzti  9295  irradd  9580  irrmul  9581  xltneg  9768  xleadd1  9807  icc0r  9858  fznuz  10033  uznfz  10034  facndiv  10648  rennim  10940  abs00ap  11000  absle  11027  cau3lem  11052  caubnd2  11055  climshft  11241  subcn2  11248  mulcn2  11249  serf0  11289  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  efieq1re  11708  moddvds  11735  dvdsssfz1  11786  nn0seqcvgd  11969  algcvgblem  11977  eucalglt  11985  lcmgcdlem  12005  rpmul  12026  divgcdcoprm0  12029  isprm6  12075  rpexp  12081  eulerthlema  12158  eulerthlemh  12159  prmdiv  12163  pcprendvds2  12219  pcz  12259  pcprmpw  12261  pcfac  12276  expnprm  12279  tgss3  12678  cnpnei  12819  cnntr  12825  hmeoopn  12911  hmeocld  12912  mulcncflem  13190  sincosq3sgn  13349  sincosq4sgn  13350  lgsdir2lem4  13532  lgsne0  13539  2sqlem8a  13558  bj-peano4  13797  iswomni0  13890