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  2070  ceqsalt  2839  sbceqal  3097  csbiebt  3177  rspcsbela  3197  preqr1g  3869  repizf2  4274  copsexg  4359  onun2  4611  suc11g  4678  elrnrexdm  5815  isoselem  5992  riotass2  6031  oawordriexmid  6702  nnm00  6762  ecopovtrn  6865  ecopovtrng  6868  infglbti  7315  difinfsnlem  7389  enq0tr  7745  addnqprl  7840  addnqpru  7841  mulnqprl  7879  mulnqpru  7880  recexprlemss1l  7946  recexprlemss1u  7947  cauappcvgprlemdisj  7962  mulextsr1lem  8091  pitonn  8159  rereceu  8200  cnegexlem1  8444  ltadd2  8689  eqord2  8754  mulext  8884  mulgt1  9133  lt2halves  9470  addltmul  9471  nzadd  9626  ltsubnn0  9641  zextlt  9666  recnz  9667  zeo  9679  peano5uzti  9682  irradd  9974  irrmul  9975  xltneg  10165  xleadd1  10204  icc0r  10255  fznuz  10432  uznfz  10433  facndiv  11097  ccatalpha  11294  swrdccatin2  11414  swrdccatin2d  11429  rennim  11680  abs00ap  11740  absle  11767  cau3lem  11792  caubnd2  11795  climshft  11982  subcn2  11989  mulcn2  11990  serf0  12030  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  efieq1re  12451  moddvds  12478  dvdsssfz1  12531  nn0seqcvgd  12731  algcvgblem  12739  eucalglt  12747  lcmgcdlem  12767  rpmul  12788  divgcdcoprm0  12791  isprm6  12837  rpexp  12843  eulerthlema  12920  eulerthlemh  12921  prmdiv  12925  pcprendvds2  12982  pcz  13023  pcprmpw  13025  pcadd2  13032  pcfac  13041  expnprm  13044  imasgrp2  13816  issubg4m  13899  znidomb  14793  tgss3  14930  cnpnei  15071  cnntr  15077  hmeoopn  15163  hmeocld  15164  mulcncflem  15459  plycolemc  15610  sincosq3sgn  15680  sincosq4sgn  15681  perfect1  15853  lgsdir2lem4  15891  lgsne0  15898  lgsquad2lem2  15942  2sqlem8a  15982  clwwlkext2edg  16404  bj-peano4  16712  iswomni0  16823