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  4246  copsexg  4330  onun2  4582  suc11g  4649  elrnrexdm  5776  isoselem  5950  riotass2  5989  oawordriexmid  6624  nnm00  6684  ecopovtrn  6787  ecopovtrng  6790  infglbti  7200  difinfsnlem  7274  enq0tr  7629  addnqprl  7724  addnqpru  7725  mulnqprl  7763  mulnqpru  7764  recexprlemss1l  7830  recexprlemss1u  7831  cauappcvgprlemdisj  7846  mulextsr1lem  7975  pitonn  8043  rereceu  8084  cnegexlem1  8329  ltadd2  8574  eqord2  8639  mulext  8769  mulgt1  9018  lt2halves  9355  addltmul  9356  nzadd  9507  ltsubnn0  9522  zextlt  9547  recnz  9548  zeo  9560  peano5uzti  9563  irradd  9849  irrmul  9850  xltneg  10040  xleadd1  10079  icc0r  10130  fznuz  10306  uznfz  10307  facndiv  10969  swrdccatin2  11269  swrdccatin2d  11284  rennim  11521  abs00ap  11581  absle  11608  cau3lem  11633  caubnd2  11636  climshft  11823  subcn2  11830  mulcn2  11831  serf0  11871  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  efieq1re  12291  moddvds  12318  dvdsssfz1  12371  nn0seqcvgd  12571  algcvgblem  12579  eucalglt  12587  lcmgcdlem  12607  rpmul  12628  divgcdcoprm0  12631  isprm6  12677  rpexp  12683  eulerthlema  12760  eulerthlemh  12761  prmdiv  12765  pcprendvds2  12822  pcz  12863  pcprmpw  12865  pcadd2  12872  pcfac  12881  expnprm  12884  imasgrp2  13655  issubg4m  13738  znidomb  14630  tgss3  14760  cnpnei  14901  cnntr  14907  hmeoopn  14993  hmeocld  14994  mulcncflem  15289  plycolemc  15440  sincosq3sgn  15510  sincosq4sgn  15511  perfect1  15680  lgsdir2lem4  15718  lgsne0  15725  lgsquad2lem2  15769  2sqlem8a  15809  bj-peano4  16342  iswomni0  16449