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  2068  ceqsalt  2828  sbceqal  3086  csbiebt  3166  rspcsbela  3186  preqr1g  3850  repizf2  4254  copsexg  4338  onun2  4590  suc11g  4657  elrnrexdm  5789  isoselem  5966  riotass2  6005  oawordriexmid  6643  nnm00  6703  ecopovtrn  6806  ecopovtrng  6809  infglbti  7229  difinfsnlem  7303  enq0tr  7659  addnqprl  7754  addnqpru  7755  mulnqprl  7793  mulnqpru  7794  recexprlemss1l  7860  recexprlemss1u  7861  cauappcvgprlemdisj  7876  mulextsr1lem  8005  pitonn  8073  rereceu  8114  cnegexlem1  8359  ltadd2  8604  eqord2  8669  mulext  8799  mulgt1  9048  lt2halves  9385  addltmul  9386  nzadd  9537  ltsubnn0  9552  zextlt  9577  recnz  9578  zeo  9590  peano5uzti  9593  irradd  9885  irrmul  9886  xltneg  10076  xleadd1  10115  icc0r  10166  fznuz  10342  uznfz  10343  facndiv  11007  ccatalpha  11199  swrdccatin2  11319  swrdccatin2d  11334  rennim  11585  abs00ap  11645  absle  11672  cau3lem  11697  caubnd2  11700  climshft  11887  subcn2  11894  mulcn2  11895  serf0  11935  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  efieq1re  12356  moddvds  12383  dvdsssfz1  12436  nn0seqcvgd  12636  algcvgblem  12644  eucalglt  12652  lcmgcdlem  12672  rpmul  12693  divgcdcoprm0  12696  isprm6  12742  rpexp  12748  eulerthlema  12825  eulerthlemh  12826  prmdiv  12830  pcprendvds2  12887  pcz  12928  pcprmpw  12930  pcadd2  12937  pcfac  12946  expnprm  12949  imasgrp2  13720  issubg4m  13803  znidomb  14696  tgss3  14831  cnpnei  14972  cnntr  14978  hmeoopn  15064  hmeocld  15065  mulcncflem  15360  plycolemc  15511  sincosq3sgn  15581  sincosq4sgn  15582  perfect1  15751  lgsdir2lem4  15789  lgsne0  15796  lgsquad2lem2  15840  2sqlem8a  15880  clwwlkext2edg  16302  bj-peano4  16610  iswomni0  16723