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  2067  ceqsalt  2826  sbceqal  3084  csbiebt  3164  rspcsbela  3184  preqr1g  3844  repizf2  4247  copsexg  4331  onun2  4583  suc11g  4650  elrnrexdm  5779  isoselem  5953  riotass2  5992  oawordriexmid  6629  nnm00  6689  ecopovtrn  6792  ecopovtrng  6795  infglbti  7208  difinfsnlem  7282  enq0tr  7637  addnqprl  7732  addnqpru  7733  mulnqprl  7771  mulnqpru  7772  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemdisj  7854  mulextsr1lem  7983  pitonn  8051  rereceu  8092  cnegexlem1  8337  ltadd2  8582  eqord2  8647  mulext  8777  mulgt1  9026  lt2halves  9363  addltmul  9364  nzadd  9515  ltsubnn0  9530  zextlt  9555  recnz  9556  zeo  9568  peano5uzti  9571  irradd  9858  irrmul  9859  xltneg  10049  xleadd1  10088  icc0r  10139  fznuz  10315  uznfz  10316  facndiv  10978  ccatalpha  11166  swrdccatin2  11282  swrdccatin2d  11297  rennim  11534  abs00ap  11594  absle  11621  cau3lem  11646  caubnd2  11649  climshft  11836  subcn2  11843  mulcn2  11844  serf0  11884  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  efieq1re  12304  moddvds  12331  dvdsssfz1  12384  nn0seqcvgd  12584  algcvgblem  12592  eucalglt  12600  lcmgcdlem  12620  rpmul  12641  divgcdcoprm0  12644  isprm6  12690  rpexp  12696  eulerthlema  12773  eulerthlemh  12774  prmdiv  12778  pcprendvds2  12835  pcz  12876  pcprmpw  12878  pcadd2  12885  pcfac  12894  expnprm  12897  imasgrp2  13668  issubg4m  13751  znidomb  14643  tgss3  14773  cnpnei  14914  cnntr  14920  hmeoopn  15006  hmeocld  15007  mulcncflem  15302  plycolemc  15453  sincosq3sgn  15523  sincosq4sgn  15524  perfect1  15693  lgsdir2lem4  15731  lgsne0  15738  lgsquad2lem2  15782  2sqlem8a  15822  clwwlkext2edg  16190  bj-peano4  16427  iswomni0  16533